A1: now

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 6
.= a * ((f . v1) + (f . w1)) by MOD_2:def 5
.= (a * (f . v1)) + (a * (f . w1)) by VECTSP_1:def 26
.= ((a * f) . v1) + (a * (f . w1)) by MATRLIN:def 6
.= ((a * f) . v1) + ((a * f) . w1) by MATRLIN:def 6 ; :: thesis: verum

end;

now

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 6
.= a * (b * (f . v1)) by MOD_2:def 5
.= (a * b) * (f . v1) by VECTSP_1:def 26
.= b * (a * (f . v1)) by VECTSP_1:def 26
.= b * ((a * f) . v1) by MATRLIN:def 6 ; :: thesis: verum

end;

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