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

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

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

let 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;

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

end;