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 A1: 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 A2: 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

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
A3: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A4: y = [y1,y2] by Lm1;
thus H1 . (x,y) = [(x1 + y1),(x2 + y2)] by A1, A3, A4
.= H2 . (x,y) by A2, A3, A4 ; :: thesis: verum

end;

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