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
A4:
( H1(G1) = D * & ( for p, q being Element of G1 holds p [*] q = p ^ q ) )
and
A5:
( H1(G2) = D * & ( for p, q being Element of G2 holds p [*] q = p ^ q ) )
; :: thesis: G1 = G2
set f1 = H2(G1);
set f2 = H2(G2);
now let a,
b be
Element of
D * ;
:: thesis: H2(G1) . a,b = H2(G2) . a,breconsider p =
a,
q =
b as
Element of
D * ;
reconsider a1 =
a,
b1 =
b as
Element of
G1 by A4;
reconsider a2 =
a,
b2 =
b as
Element of
G2 by A5;
(
H2(
G2)
. a,
b = a2 [*] b2 &
a2 [*] b2 = p ^ q &
H2(
G1)
. a,
b = a1 [*] b1 &
a1 [*] b1 = p ^ q )
by A4, A5;
hence
H2(
G1)
. a,
b = H2(
G2)
. a,
b
;
:: thesis: verum end;
hence
G1 = G2
by A4, A5, BINOP_1:2; :: thesis: verum