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
A9: the carrier of G1 = the carrier of X and
A10: for x, y being Element of X holds the addF of G1 . x,y = x \ ((0. X) \ y) and
A11: 0. G1 = 0. X and
A12: the carrier of G2 = the carrier of X and
A13: for x, y being Element of X holds the addF of G2 . x,y = x \ ((0. X) \ y) and
A14: 0. G2 = 0. X ; :: thesis: G1 = G2

now

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 A9;
thus the addF of G1 . a,b = x \ ((0. X) \ y) by A10
.= the addF of G2 . a,b by A13 ; :: thesis: verum

end;

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

end;