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 ((f1 + f2) * g) = [#] V1 & dom ((f1 * g) + (f2 * g)) = [#] V1 & dom g = [#] V1 ) by FUNCT_2:def 1;

now

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

end;

hence (f1 + f2) * g = (f1 * g) + (f2 * g) by A1, FUNCT_1:9; :: thesis: verum