let K be Field; :: thesis: for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 st g is additive & g is homogeneous holds
g * (f1 + f2) = (g * f1) + (g * f2)
let V1 be VectSp of K; :: thesis: for f1, f2, g being Function of V1,V1 st g is additive & g is homogeneous holds
g * (f1 + f2) = (g * f1) + (g * f2)
let f1, f2, g be Function of V1,V1; :: thesis: ( g is additive & g is homogeneous implies g * (f1 + f2) = (g * f1) + (g * f2) )
assume A1: ( g is additive & g is homogeneous ) ; :: thesis: g * (f1 + f2) = (g * f1) + (g * f2)
A2: dom (g * (f1 + f2)) = [#] V1 by FUNCT_2:def 1;
A3: dom f2 = [#] V1 by FUNCT_2:def 1;
A4: dom f1 = [#] V1 by FUNCT_2:def 1;

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

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

end;

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