let K be Field; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( f is additive & f is homogeneous implies L * (f * g) = f * (L * g) )
assume A1: ( f is additive & f is homogeneous ) ; :: thesis: 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;

A4: now :: thesis: for x being object st x in dom (L * (f * g)) holds
(L * (f * g)) . x = (f * (L * g)) . x

let x be object ; :: thesis: ( x in dom (L * (f * g)) implies (L * (f * g)) . x = (f * (L * g)) . x )
assume x in dom (L * (f * g)) ; :: thesis: (L * (f * g)) . x = (f * (L * g)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def 1;
thus (L * (f * g)) . x = L * ((f * g) . v) by MATRLIN:def 4
.= L * (f . (g . v)) by A3, FUNCT_1:13
.= f . (L * (g . v)) by A1, MOD_2:def 2
.= f . ((L * g) . v) by MATRLIN:def 4
.= (f * (L * g)) . x by A2, FUNCT_1:12 ; :: thesis: verum

end;

dom (L * (f * g)) = [#] V1 by FUNCT_2:def 1;
hence L * (f * g) = f * (L * g) by A2, A4, FUNCT_1:2; :: thesis: verum