let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)
let f be linear-transformation of V1,V1; :: thesis: for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)
let a, b be Scalar of K; :: thesis: (a + b) * f = (a * f) + (b * f)
A1: ( dom ((a + b) * f) = [#] V1 & dom ((a * f) + (b * f)) = [#] V1 ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in dom ((a + b) * f) implies ((a + b) * f) . x = ((a * f) + (b * f)) . x )
assume A2: x in dom ((a + b) * f) ; :: thesis: ((a + b) * f) . x = ((a * f) + (b * f)) . x
reconsider v = x as Element of V1 by A2, FUNCT_2:def 1;
thus ((a + b) * f) . x = (a + b) * (f . v) by MATRLIN:def 6
.= (a * (f . v)) + (b * (f . v)) by VECTSP_1:def 26
.= ((a * f) . v) + (b * (f . v)) by MATRLIN:def 6
.= ((a * f) . v) + ((b * f) . v) by MATRLIN:def 6
.= ((a * f) + (b * f)) . x by MATRLIN:def 5 ; :: thesis: verum

end;

hence (a + b) * f = (a * f) + (b * f) by A1, FUNCT_1:9; :: thesis: verum