set M = the MonoidalExtension of G;
A1: now :: thesis: ( ex M being multLoopStr st G = M implies ex M being multLoopStr st
( H2(M) c= H2(G) & ( for N being multLoopStr st G = N holds
H3(M) = H3(N) ) ) )
given M being multLoopStr such that A2: G = M ; :: thesis: ex M being multLoopStr st
( H2(M) c= H2(G) & ( for N being multLoopStr st G = N holds
H3(M) = H3(N) ) )
take M = M; :: thesis: ( H2(M) c= H2(G) & ( for N being multLoopStr st G = N holds
H3(M) = H3(N) ) )
thus H2(M) c= H2(G) by A2; :: thesis: for N being multLoopStr st G = N holds
H3(M) = H3(N)
thus for N being multLoopStr st G = N holds
H3(M) = H3(N) by A2; :: thesis: verum
end;
A3: ( ex M being multLoopStr st G = M or for N being multLoopStr st G = N holds
H3( the MonoidalExtension of G) = H3(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 b1 being multLoopStr st
( the multF of b1 c= the multF of G & ( for M being multLoopStr st G = M holds
1. b1 = 1. M ) ) by A1, A3; :: thesis: verum