let K be Field; :: thesis: for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)
let V1 be VectSp of K; :: thesis: for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)
let f1, f2, g be Function of V1,V1; :: thesis: (f1 + f2) * g = (f1 * g) + (f2 * g)
A1: dom g = [#] V1 by FUNCT_2:def 1;
A2: dom ((f1 + f2) * g) = [#] V1 by FUNCT_2:def 1;

A3: now :: thesis: for x being set st x in dom g holds
((f1 + f2) * g) . x = ((f1 * g) + (f2 * g)) . x

let x be set ; :: thesis: ( x in dom g implies ((f1 + f2) * g) . x = ((f1 * g) + (f2 * g)) . x )
assume x in dom g ; :: thesis: ((f1 + f2) * g) . x = ((f1 * g) + (f2 * g)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def 1;
thus ((f1 + f2) * g) . x = (f1 + f2) . (g . v) by A2, FUNCT_1:12
.= (f1 . (g . v)) + (f2 . (g . v)) by MATRLIN:def 3
.= ((f1 * g) . v) + (f2 . (g . v)) by A1, FUNCT_1:13
.= ((f1 * g) . v) + ((f2 * g) . v) by A1, FUNCT_1:13
.= ((f1 * g) + (f2 * g)) . x by MATRLIN:def 3 ; :: thesis: verum

end;

dom ((f1 * g) + (f2 * g)) = [#] V1 by FUNCT_2:def 1;
hence (f1 + f2) * g = (f1 * g) + (f2 * g) by A2, A1, A3, FUNCT_1:2; :: thesis: verum