let R be commutative Ring; :: thesis: for U, V being VectSp of R
for f being linear-transformation of U,V
for a being Element of R holds a '*' f is linear-transformation of U,V
let U, V be VectSp of R; :: thesis: for f being linear-transformation of U,V
for a being Element of R holds a '*' f is linear-transformation of U,V
let f be linear-transformation of U,V; :: thesis: for a being Element of R holds a '*' f is linear-transformation of U,V
let a be Element of R; :: thesis: a '*' f is linear-transformation of U,V

A: now :: thesis: for x, y being Element of U holds (a '*' f) . (x + y) = ((a '*' f) . x) + ((a '*' f) . y)

let x, y be Element of U; :: thesis: (a '*' f) . (x + y) = ((a '*' f) . x) + ((a '*' f) . y)
thus (a '*' f) . (x + y) = a * (f . (x + y)) by defmu
.= a * ((f . x) + (f . y)) by VECTSP_1:def 20
.= (a * (f . x)) + (a * (f . y)) by VECTSP_1:def 14
.= ((a '*' f) . x) + (a * (f . y)) by defmu
.= ((a '*' f) . x) + ((a '*' f) . y) by defmu ; :: thesis: verum

end;

now :: thesis: for b being Element of R
for x being Element of U holds (a '*' f) . (b * x) = b * ((a '*' f) . x)

let b be Element of R; :: thesis: for x being Element of U holds (a '*' f) . (b * x) = b * ((a '*' f) . x)
let x be Element of U; :: thesis: (a '*' f) . (b * x) = b * ((a '*' f) . x)
thus (a '*' f) . (b * x) = a * (f . (b * x)) by defmu
.= a * (b * (f . x)) by MOD_2:def 2
.= (a * b) * (f . x) by VECTSP_1:def 16
.= b * (a * (f . x)) by VECTSP_1:def 16
.= b * ((a '*' f) . x) by defmu ; :: thesis: verum

end;

hence a '*' f is linear-transformation of U,V by A, MOD_2:def 2, VECTSP_1:def 20; :: thesis: verum