let a be Element of K; :: according to VECTSP_1:def 13 :: thesis: for b_{1}, b_{2} being Element of the carrier of [:G,F:] holds a * (b_{1} + b_{2}) = (a * b_{1}) + (a * b_{2})

let x, y be Vector of [:G,F:]; :: thesis: a * (x + y) = (a * x) + (a * y)

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;

A3: ( a * (x1 + y1) = (a * x1) + (a * y1) & a * (x2 + y2) = (a * x2) + (a * y2) ) by VECTSP_1:def 14;

thus a * (x + y) = (prod_MLT (G,F)) . (a,[(x1 + y1),(x2 + y2)]) by A1, A2, PRVECT_3:def 1

.= [(a * (x1 + y1)),(a * (x2 + y2))] by YDef2

.= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(a * y1),(a * y2)]) by A3, PRVECT_3:def 1

.= (prod_ADD (G,F)) . (((prod_MLT (G,F)) . (a,[x1,x2])),[(a * y1),(a * y2)]) by YDef2

.= (a * x) + (a * y) by A1, A2, YDef2 ; :: thesis: verum

let x, y be Vector of [:G,F:]; :: thesis: a * (x + y) = (a * x) + (a * y)

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;

A3: ( a * (x1 + y1) = (a * x1) + (a * y1) & a * (x2 + y2) = (a * x2) + (a * y2) ) by VECTSP_1:def 14;

thus a * (x + y) = (prod_MLT (G,F)) . (a,[(x1 + y1),(x2 + y2)]) by A1, A2, PRVECT_3:def 1

.= [(a * (x1 + y1)),(a * (x2 + y2))] by YDef2

.= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(a * y1),(a * y2)]) by A3, PRVECT_3:def 1

.= (prod_ADD (G,F)) . (((prod_MLT (G,F)) . (a,[x1,x2])),[(a * y1),(a * y2)]) by YDef2

.= (a * x) + (a * y) by A1, A2, YDef2 ; :: thesis: verum