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:

proof

let G1, G2 be strict AbGroup; :: thesis:
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:

now :: thesis:

let a, b be Element of G1; :: thesis:
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:

end;

hence G1 = G2 by A7, A9, A11, BINOP_1:2; :: thesis:

end;