let x, y, z be Element of [:G,F:]; RLVECT_1:def 6 (x + y) + z = x + (y + z)
consider x1 being Point of G, x2 being Point of F such that
P1:
x = [x1,x2]
by LM01;
consider y1 being Point of G, y2 being Point of F such that
P2:
y = [y1,y2]
by LM01;
consider z1 being Point of G, z2 being Point of F such that
P3:
z = [z1,z2]
by LM01;
A1:
( (x1 + y1) + z1 = x1 + (y1 + z1) & (x2 + y2) + z2 = x2 + (y2 + z2) )
by RLVECT_1:def 6;
thus (x + y) + z =
(prod_ADD (G,F)) . ([(x1 + y1),(x2 + y2)],[z1,z2])
by P1, P2, P3, defADD
.=
[((x1 + y1) + z1),((x2 + y2) + z2)]
by defADD
.=
(prod_ADD (G,F)) . ([x1,x2],[(y1 + z1),(y2 + z2)])
by A1, defADD
.=
x + (y + z)
by P1, P2, P3, defADD
; verum