let x, y, z be Element of [:G,F:]; RLVECT_1:def 3 (x + y) + z = x + (y + z)
consider x1 being Vector of G, x2 being Vector of F such that
A1:
x = [x1,x2]
by SUBSET_1:43;
consider y1 being Vector of G, y2 being Vector of F such that
A2:
y = [y1,y2]
by SUBSET_1:43;
consider z1 being Vector of G, z2 being Vector of F such that
A3:
z = [z1,z2]
by SUBSET_1:43;
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, PRVECT_3:def 1
.=
[(x1 + (y1 + z1)),(x2 + (y2 + z2))]
by A4, PRVECT_3:def 1
.=
(prod_ADD (G,F)) . ([x1,x2],[(y1 + z1),(y2 + z2)])
by PRVECT_3:def 1
.=
x + (y + z)
by A1, A2, A3, PRVECT_3:def 1
; verum