A1: now

let v1, w1 be Vector of V1; :: thesis: (f + g) . (v1 + w1) = ((f + g) . v1) + ((f + g) . w1)
thus (f + g) . (v1 + w1) = (f . (v1 + w1)) + (g . (v1 + w1)) by MATRLIN:def 5
.= ((f . v1) + (f . w1)) + (g . (v1 + w1)) by MOD_2:def 5
.= ((f . v1) + (f . w1)) + ((g . v1) + (g . w1)) by MOD_2:def 5
.= (f . v1) + ((f . w1) + ((g . v1) + (g . w1))) by RLVECT_1:def 6
.= (f . v1) + ((g . v1) + ((g . w1) + (f . w1))) by RLVECT_1:def 6
.= ((f . v1) + (g . v1)) + ((f . w1) + (g . w1)) by RLVECT_1:def 6
.= ((f + g) . v1) + ((f . w1) + (g . w1)) by MATRLIN:def 5
.= ((f + g) . v1) + ((f + g) . w1) by MATRLIN:def 5 ; :: thesis: verum

end;

now

let a be Scalar of K; :: thesis: for v1 being Vector of V1 holds (f + g) . (a * v1) = a * ((f + g) . v1)
let v1 be Vector of V1; :: thesis: (f + g) . (a * v1) = a * ((f + g) . v1)
thus (f + g) . (a * v1) = (f . (a * v1)) + (g . (a * v1)) by MATRLIN:def 5
.= (a * (f . v1)) + (g . (a * v1)) by MOD_2:def 5
.= (a * (f . v1)) + (a * (g . v1)) by MOD_2:def 5
.= a * ((f . v1) + (g . v1)) by VECTSP_1:def 26
.= a * ((f + g) . v1) by MATRLIN:def 5 ; :: thesis: verum

end;

hence f + g is linear-transformation of V1,V2 by A1, MOD_2:def 5; :: thesis: verum