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

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

consider x1 being Vector of G, x2 being Vector of F such that

A1: x = [x1,x2] by SUBSET_1:43;

A2: ( (a + b) * x1 = (a * x1) + (b * x1) & (a + b) * x2 = (a * x2) + (b * x2) ) by VECTSP_1:def 15;

thus (a + b) * x = [((a + b) * x1),((a + b) * x2)] by A1, YDef2

.= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(b * x1),(b * x2)]) by A2, PRVECT_3:def 1

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

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

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

consider x1 being Vector of G, x2 being Vector of F such that

A1: x = [x1,x2] by SUBSET_1:43;

A2: ( (a + b) * x1 = (a * x1) + (b * x1) & (a + b) * x2 = (a * x2) + (b * x2) ) by VECTSP_1:def 15;

thus (a + b) * x = [((a + b) * x1),((a + b) * x2)] by A1, YDef2

.= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(b * x1),(b * x2)]) by A2, PRVECT_3:def 1

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

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