let K be Field; 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; 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; ( g is additive & g is homogeneous implies g * (f1 + f2) = (g * f1) + (g * f2) )
assume A1:
( g is additive & g is homogeneous )
; 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;
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; verum