let G1, G2 be non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma ; ( 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:
H1(G1) = D *
and
A7:
for p, q being Element of G1 holds p [*] q = p ^ q
and
A8:
H1(G2) = D *
and
A9:
for p, q being Element of G2 holds p [*] q = p ^ q
; G1 = G2
set f1 = H2(G1);
set f2 = H2(G2);
now for a, b being Element of D * holds H2(G1) . (a,b) = H2(G2) . (a,b)let a,
b be
Element of
D * ;
H2(G1) . (a,b) = H2(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
H2(
G1)
. (
a,
b)
= H2(
G2)
. (
a,
b)
;
verum end;
hence
G1 = G2
by A6, A8, BINOP_1:2; verum