let a0 be Real; :: according to RLVECT_1:def 5 :: thesis: for b₁, b₂ being Element of the carrier of [:G,F:] holds a0 * (b₁ + b₂) = (a0 * b₁) + (a0 * b₂)
let x, y be VECTOR of [:G,F:]; :: thesis: a0 * (x + y) = (a0 * x) + (a0 * y)
reconsider a = a0 as Element of REAL by XREAL_0:def 1;
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;
A3: ( a * (x1 + y1) = (a0 * x1) + (a0 * y1) & a * (x2 + y2) = (a0 * x2) + (a0 * y2) ) by RLVECT_1:def 5;
thus a0 * (x + y) = (prod_MLT (G,F)) . (a,[(x1 + y1),(x2 + y2)]) by A1, A2, Def1
.= [(a * (x1 + y1)),(a * (x2 + y2))] by Def2
.= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(a * y1),(a * y2)]) by A3, Def1
.= (prod_ADD (G,F)) . (((prod_MLT (G,F)) . (a,[x1,x2])),[(a * y1),(a * y2)]) by Def2
.= (a0 * x) + (a0 * y) by A1, A2, Def2 ; :: thesis: verum