let H1, H2 be BinOp of [: the carrier of G, the carrier of F:]; :: thesis: ( ( for g1, g2 being Point of G
for f1, f2 being Point of F holds H1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) & ( for g1, g2 being Point of G
for f1, f2 being Point of F holds H2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) implies H1 = H2 )
assume A7: for g1, g2 being Point of G
for f1, f2 being Point of F holds H1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ; :: thesis: ( ex g1, g2 being Point of G ex f1, f2 being Point of F st not H2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] or H1 = H2 )
assume A8: for g1, g2 being Point of G
for f1, f2 being Point of F holds H2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ; :: thesis: H1 = H2

now :: thesis: for x, y being Element of [: the carrier of G, the carrier of F:] holds H1 . (x,y) = H2 . (x,y)

let x, y be Element of [: the carrier of G, the carrier of F:]; :: thesis: H1 . (x,y) = H2 . (x,y)
consider x1 being Point of G, x2 being Point of F such that
A9: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A10: y = [y1,y2] by Lm1;
thus H1 . (x,y) = [(x1 + y1),(x2 + y2)] by A7, A9, A10
.= H2 . (x,y) by A8, A9, A10 ; :: thesis: verum

end;

hence H1 = H2 by BINOP_1:2; :: thesis: verum