let a0, b0 be real number ; :: according to RLVECT_1:def 9 :: thesis: for b₁ being Element of the carrier of [:G,F:] holds (a0 + b0) * b₁ = (a0 * b₁) + (b0 * b₁)
let x be VECTOR of [:G,F:]; :: thesis: (a0 + b0) * x = (a0 * x) + (b0 * x)
reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def 1;
consider x1 being Point of G, x2 being Point of F such that
P1: x = [x1,x2] by LM01;
P3: ( (a + b) * x1 = (a0 * x1) + (b0 * x1) & (a + b) * x2 = (a0 * x2) + (b0 * x2) ) by RLVECT_1:def 9;
thus (a0 + b0) * x = [((a + b) * x1),((a + b) * x2)] by P1, defMLT
.= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(b * x1),(b * x2)]) by P3, defADD
.= (prod_ADD (G,F)) . (((prod_MLT (G,F)) . (a,[x1,x2])),[(b * x1),(b * x2)]) by defMLT
.= (a0 * x) + (b0 * x) by P1, defMLT ; :: thesis: verum