A1: now :: thesis: for a being Scalar of K
for v1 being Vector of V1 holds (f + g) . (a * v1) = a * ((f + g) . v1)

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 3
.= (a * (f . v1)) + (g . (a * v1)) by MOD_2:def 2
.= (a * (f . v1)) + (a * (g . v1)) by MOD_2:def 2
.= a * ((f . v1) + (g . v1)) by VECTSP_1:def 14
.= a * ((f + g) . v1) by MATRLIN:def 3 ; :: thesis: verum

end;

now :: thesis: for v1, w1 being Vector of V1 holds (f + g) . (v1 + w1) = ((f + g) . v1) + ((f + g) . w1)

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 3
.= ((f . v1) + (f . w1)) + (g . (v1 + w1)) by VECTSP_1:def 20
.= ((f . v1) + (f . w1)) + ((g . v1) + (g . w1)) by VECTSP_1:def 20
.= (f . v1) + ((f . w1) + ((g . v1) + (g . w1))) by RLVECT_1:def 3
.= (f . v1) + ((g . v1) + ((g . w1) + (f . w1))) by RLVECT_1:def 3
.= ((f . v1) + (g . v1)) + ((f . w1) + (g . w1)) by RLVECT_1:def 3
.= ((f + g) . v1) + ((f . w1) + (g . w1)) by MATRLIN:def 3
.= ((f + g) . v1) + ((f + g) . w1) by MATRLIN:def 3 ; :: thesis: verum

end;

then ( f + g is additive & f + g is homogeneous ) by A1, MOD_2:def 2;
hence ( f + g is homogeneous & f + g is additive ) ; :: thesis: verum