thus
for G1, G2 being strict AbGroup st the carrier of G1 = the carrier of X & ( for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) ) & 0. G1 = 0. X & the carrier of G2 = the carrier of X & ( for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) ) & 0. G2 = 0. X holds

G1 = G2 :: thesis: verum

G1 = G2 :: thesis: verum

proof

let G1, G2 be strict AbGroup; :: thesis: ( the carrier of G1 = the carrier of X & ( for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) ) & 0. G1 = 0. X & the carrier of G2 = the carrier of X & ( for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) ) & 0. G2 = 0. X implies G1 = G2 )

assume that

A7: the carrier of G1 = the carrier of X and

A8: for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) and

A9: ( 0. G1 = 0. X & the carrier of G2 = the carrier of X ) and

A10: for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) and

A11: 0. G2 = 0. X ; :: thesis: G1 = G2

end;assume that

A7: the carrier of G1 = the carrier of X and

A8: for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) and

A9: ( 0. G1 = 0. X & the carrier of G2 = the carrier of X ) and

A10: for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) and

A11: 0. G2 = 0. X ; :: thesis: G1 = G2

now :: thesis: for a, b being Element of G1 holds the addF of G1 . (a,b) = the addF of G2 . (a,b)

hence
G1 = G2
by A7, A9, A11, BINOP_1:2; :: thesis: verumlet a, b be Element of G1; :: thesis: the addF of G1 . (a,b) = the addF of G2 . (a,b)

reconsider x = a, y = b as Element of X by A7;

thus the addF of G1 . (a,b) = x \ ((0. X) \ y) by A8

.= the addF of G2 . (a,b) by A10 ; :: thesis: verum

end;reconsider x = a, y = b as Element of X by A7;

thus the addF of G1 . (a,b) = x \ ((0. X) \ y) by A8

.= the addF of G2 . (a,b) by A10 ; :: thesis: verum