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: now :: thesis: for x being object st x in dom ((a + b) * f) holds
((a + b) * f) . x = ((a * f) + (b * f)) . x

let x be object ; :: thesis: ( x in dom ((a + b) * f) implies ((a + b) * f) . x = ((a * f) + (b * f)) . x )
assume x in dom ((a + b) * f) ; :: thesis: ((a + b) * f) . x = ((a * f) + (b * f)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def 1;
thus ((a + b) * f) . x = (a + b) * (f . v) by MATRLIN:def 4
.= (a * (f . v)) + (b * (f . v)) by VECTSP_1:def 15
.= ((a * f) . v) + (b * (f . v)) by MATRLIN:def 4
.= ((a * f) . v) + ((b * f) . v) by MATRLIN:def 4
.= ((a * f) + (b * f)) . x by MATRLIN:def 3 ; :: thesis: verum

end;

( dom ((a + b) * f) = [#] V1 & dom ((a * f) + (b * f)) = [#] V1 ) by FUNCT_2:def 1;
hence (a + b) * f = (a * f) + (b * f) by A1, FUNCT_1:2; :: thesis: verum