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

let b be Scalar of K; :: thesis: for v1 being Vector of V1 holds (a * f) . (b * v1) = b * ((a * f) . v1)
let v1 be Vector of V1; :: thesis: (a * f) . (b * v1) = b * ((a * f) . v1)
thus (a * f) . (b * v1) = a * (f . (b * v1)) by MATRLIN:def 4
.= a * (b * (f . v1)) by MOD_2:def 2
.= (a * b) * (f . v1) by VECTSP_1:def 16
.= b * (a * (f . v1)) by VECTSP_1:def 16
.= b * ((a * f) . v1) by MATRLIN:def 4 ; :: thesis: verum

end;

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

let v1, w1 be Vector of V1; :: thesis: (a * f) . (v1 + w1) = ((a * f) . v1) + ((a * f) . w1)
thus (a * f) . (v1 + w1) = a * (f . (v1 + w1)) by MATRLIN:def 4
.= a * ((f . v1) + (f . w1)) by VECTSP_1:def 20
.= (a * (f . v1)) + (a * (f . w1)) by VECTSP_1:def 14
.= ((a * f) . v1) + (a * (f . w1)) by MATRLIN:def 4
.= ((a * f) . v1) + ((a * f) . w1) by MATRLIN:def 4 ; :: thesis: verum

end;

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