let x, y, z be Element of [:G,F:]; :: according to RLVECT_1:def 3 :: thesis: (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 ; :: thesis: verum

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 ; :: thesis: verum