set M = the MonoidalExtension of G;

A1: now :: thesis: ( ex M being multLoopStr st G = M implies ex M being multLoopStr st
( H₂(M) c= H₂(G) & ( for N being multLoopStr st G = N holds
H₃(M) = H₃(N) ) ) )

given M being multLoopStr such that A2: G = M ; :: thesis: ex M being multLoopStr st
( H₂(M) c= H₂(G) & ( for N being multLoopStr st G = N holds
H₃(M) = H₃(N) ) )
take M = M; :: thesis: ( H₂(M) c= H₂(G) & ( for N being multLoopStr st G = N holds
H₃(M) = H₃(N) ) )
thus H₂(M) c= H₂(G) by A2; :: thesis: for N being multLoopStr st G = N holds
H₃(M) = H₃(N)
thus for N being multLoopStr st G = N holds
H₃(M) = H₃(N) by A2; :: thesis: verum

end;

A3: ( ex M being multLoopStr st G = M or for N being multLoopStr st G = N holds
H₃( the MonoidalExtension of G) = H₃(N) ) ;
multMagma(# the carrier of the MonoidalExtension of G, the multF of the MonoidalExtension of G #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence ex b₁ being multLoopStr st
( the multF of b₁ c= the multF of G & ( for M being multLoopStr st G = M holds
1. b₁ = 1. M ) ) by A1, A3; :: thesis: verum