let M1, M2 be non empty strict multMagma ; :: thesis: ( the carrier of M1 = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of M1 . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) & the carrier of M2 = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of M2 . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) implies M1 = M2 )
assume that
A1: ( the carrier of M1 = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of M1 . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) ) and
A2: ( the carrier of M2 = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of M2 . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) ) ; :: thesis: M1 = M2
for x, y being set st x in the carrier of M1 & y in the carrier of M1 holds
the multF of M1 . (x,y) = the multF of M2 . (x,y)

proof

let x, y be set ; :: thesis: ( x in the carrier of M1 & y in the carrier of M1 implies the multF of M1 . (x,y) = the multF of M2 . (x,y) )
assume B1: x in the carrier of M1 ; :: thesis: ( not y in the carrier of M1 or the multF of M1 . (x,y) = the multF of M2 . (x,y) )
assume y in the carrier of M1 ; :: thesis: the multF of M1 . (x,y) = the multF of M2 . (x,y)
then reconsider f = x, g = y as Element of product (Carrier <*G,A*>) by A1, B1;
consider h1 being Function, a11 being Element of A, g12 being Element of G such that
B3: ( h1 = the multF of M1 . (f,g) & a11 = f . 2 & g12 = g . 1 & h1 . 1 = the multF of G . ((f . 1),((phi . a11) . g12)) & h1 . 2 = the multF of A . ((f . 2),(g . 2)) ) by A1;
consider h2 being Function, a21 being Element of A, g22 being Element of G such that
B4: ( h2 = the multF of M2 . (f,g) & a21 = f . 2 & g22 = g . 1 & h2 . 1 = the multF of G . ((f . 1),((phi . a21) . g22)) & h2 . 2 = the multF of A . ((f . 2),(g . 2)) ) by A2;
B5: ( dom h1 = {1,2} & dom h2 = {1,2} )

proof

h1 in product (Carrier <*G,A*>) by A1, B3, BINOP_1:17;
then ex f1 being Function st
( h1 = f1 & dom f1 = dom (Carrier <*G,A*>) & ( for y1 being object st y1 in dom (Carrier <*G,A*>) holds
f1 . y1 in (Carrier <*G,A*>) . y1 ) ) by CARD_3:def 5;
hence dom h1 = {1,2} by PARTFUN1:def 2; :: thesis: dom h2 = {1,2}
h2 in product (Carrier <*G,A*>) by A2, B4, BINOP_1:17;
then ex f1 being Function st
( h2 = f1 & dom f1 = dom (Carrier <*G,A*>) & ( for y1 being object st y1 in dom (Carrier <*G,A*>) holds
f1 . y1 in (Carrier <*G,A*>) . y1 ) ) by CARD_3:def 5;
hence dom h2 = {1,2} by PARTFUN1:def 2; :: thesis: verum

end;

for i being object st i in dom h1 holds
h1 . i = h2 . i

proof

let i be object ; :: thesis: ( i in dom h1 implies h1 . i = h2 . i )
assume i in dom h1 ; :: thesis: h1 . i = h2 . i

per cases then ( i = 1 or i = 2 ) by B5, TARSKI:def 2;

suppose i = 1 ; :: thesis: h1 . i = h2 . i

hence h1 . i = h2 . i by B3, B4; :: thesis: verum

end;

suppose i = 2 ; :: thesis: h1 . i = h2 . i

hence h1 . i = h2 . i by B3, B4; :: thesis: verum

end;

end;

end;

hence the multF of M1 . (x,y) = the multF of M2 . (x,y) by B3, B4, B5, FUNCT_1:def 11; :: thesis: verum

end;

hence M1 = M2 by A1, A2, BINOP_1:1; :: thesis: verum