let x, y, z be Element of [:G,F:]; RLVECT_1:def 3 (x + y) + z = x + (y + z)
consider x1 being Point of G, x2 being Point of F such that
A1:
x = [x1,x2]
by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A2:
y = [y1,y2]
by Lm1;
consider z1 being Point of G, z2 being Point of F such that
A3:
z = [z1,z2]
by Lm1;
A4:
( (x1 + y1) + z1 = x1 + (y1 + z1) & (x2 + y2) + z2 = x2 + (y2 + z2) )
by RLVECT_1:def 3;
thus (x + y) + z =
(prod_ADD (G,F)) . ([(x1 + y1),(x2 + y2)],[z1,z2])
by A1, A2, A3, Def1
.=
[((x1 + y1) + z1),((x2 + y2) + z2)]
by Def1
.=
(prod_ADD (G,F)) . ([x1,x2],[(y1 + z1),(y2 + z2)])
by A4, Def1
.=
x + (y + z)
by A1, A2, A3, Def1
; verum