[00FU]
Proof.
We first prove part ([00FR]). By lemma 7.2.4, the \(\infty\)-category \(\underline{\nabla_2 \otimes \mathbb E_0}\) is equivalent to the walking span 
and hence the \(\infty\)-operad 
corepresents spans of \(\mathbb E_1\)-morphisms.
On underlying categories, the operad map \(\underline{\nabla_2 \otimes \mathbb E_0} \otimes \mathbb E_1 \rightarrow\nabla_2 \otimes \mathbb E_1\) is the identity. It therefore suffices to show that the induced maps on multi-hom spaces are \((-1)\)-connected. Denote the colors of 
by \(A, C\) and \(B\), the morphisms by 
, the multiplication cells by 
, 
and 
, the unit cells by 
and 
and use the same notation for their respective images in \(\nabla_2 \otimes \mathbb E_1\). The only generating cell of \(\nabla_2 \otimes \mathbb E_1\) that is not evidently in the image of is the binary multiplication stemming from the \(\nabla_2\)-operad, which we denote by \(\mu \in \mathrm{Mul}_{\nabla_2 \otimes \mathbb E_1}(A,B;C)\). We will now show that this additional generator \(\mu\) is also in the image of 
which concludes the proof that 
induces (-1)-connected maps on all multi-hom spaces.
Since \(\mu\) is a map of \(\mathbb E_1\)-algebras, we have a path in \(\mathrm{Mul}_{\nabla_2 \otimes \mathbb E_1}(A,A, B, B;C)\) (where we abuse notation and write \(- \circ (-\otimes-)\) to denote the evident operadic compositions): \[\mu\circ(\mu_A\otimes \mu_B)\simeq \mu_C\circ (\mu\otimes \mu).\] On the other hand, left and right unitality produce paths in \(\mathrm{Mul}_{\nabla_2\otimes \mathbb E_1}(A;C)\) and \(\mathrm{Mul}_{\nabla_2\otimes \mathbb E_1}(B;C)\), respectively : \[\mu\circ (\mathrm{id}_A\otimes 1_B)\simeq f \hspace{1cm} \mu\circ (1_A \otimes \mathrm{id}_B)\simeq g .\] Composing these, we conclude: \[\mu\simeq \mu\circ(\mu_A\otimes\mu_B)\circ(\mathrm{id}_A \otimes 1_A\otimes 1_B\otimes \mathrm{id}_B)\simeq\mu_C\circ(\mu\otimes \mu)\circ (\mathrm{id}_A \otimes 1_A\otimes 1_B\otimes \mathrm{id}_B)\simeq\mu_C\circ(f\otimes g)\] Hence, \(\mu\) is in the image of 
Since \(\mathrm{Op}\) is a presentably monoidal category, the pushout squares ([00E7]) induce pushout squares 
Since left class in a factorization system is preserved under pushouts, so \([1] \otimes \mathbb E_1 \rightarrow\mathbb T_2 \otimes \mathbb E_1\) and \(\mathbb E_1 \rightarrow\mathbb A_2 \otimes \mathbb E_1\) are also \(0\)-surjective. ◻