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 linear 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 linear 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 linear holds
L * (f * g) = f * (L * g)
let f, g be Function of V1,V1; :: thesis: ( f is linear implies L * (f * g) = f * (L * g) )
assume A1: f is linear ; :: 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

let x be set ; :: 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 6
.= L * (f . (g . v)) by A3, FUNCT_1:23
.= f . (L * (g . v)) by A1, MOD_2:def 5
.= f . ((L * g) . v) by MATRLIN:def 6
.= (f * (L * g)) . x by A2, FUNCT_1:22 ; :: 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:9; :: thesis: verum