let G1, G2 be non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma ; :: thesis: ( the carrier of G1 = D * & ( for p, q being Element of G1 holds p [*] q = p ^ q ) & the carrier of G2 = D * & ( for p, q being Element of G2 holds p [*] q = p ^ q ) implies G1 = G2 )
assume that
A6: H₁(G1) = D * and
A7: for p, q being Element of G1 holds p [*] q = p ^ q and
A8: H₁(G2) = D * and
A9: for p, q being Element of G2 holds p [*] q = p ^ q ; :: thesis: G1 = G2
set f1 = H₂(G1);
set f2 = H₂(G2);

now

let a, b be Element of D * ; :: thesis: H₂(G1) . a,b = H₂(G2) . a,b
reconsider a2 = a, b2 = b as Element of G2 by A8;
reconsider a1 = a, b1 = b as Element of G1 by A6;
reconsider p = a, q = b as Element of D * ;
( a2 [*] b2 = p ^ q & a1 [*] b1 = p ^ q ) by A7, A9;
hence H₂(G1) . a,b = H₂(G2) . a,b ; :: thesis: verum

end;

hence G1 = G2 by A6, A8, BINOP_1:2; :: thesis: verum