let H1, H2 be BinOp of [: the carrier of G, the carrier of F:]; ( ( 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)]
; ( 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)]
; H1 = H2
now 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:];
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
;
verum end;
hence
H1 = H2
; verum