let K be Field; for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 st f is additive & f is homogeneous holds
L * (f * g) = f * (L * g)
let V1 be VectSp of K; for L being Scalar of K
for f, g being Function of V1,V1 st f is additive & f is homogeneous holds
L * (f * g) = f * (L * g)
let L be Scalar of K; for f, g being Function of V1,V1 st f is additive & f is homogeneous holds
L * (f * g) = f * (L * g)
let f, g be Function of V1,V1; ( f is additive & f is homogeneous implies L * (f * g) = f * (L * g) )
assume A1:
( f is additive & f is homogeneous )
; L * (f * g) = f * (L * g)
A2:
dom (f * (L * g)) = [#] V1
by FUNCT_2:def 1;
A3:
dom g = [#] V1
by FUNCT_2:def 1;
dom (L * (f * g)) = [#] V1
by FUNCT_2:def 1;
hence
L * (f * g) = f * (L * g)
by A2, A4, FUNCT_1:2; verum