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 holds L * (f * g) = (L * f) * g
let V1 be VectSp of K; :: thesis: for L being Scalar of K
for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g
let L be Scalar of K; :: thesis: for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g
let f, g be Function of V1,V1; :: thesis: L * (f * g) = (L * f) * g
A1: dom ((L * f) * g) = [#] V1 by FUNCT_2:def 1;
A2: dom g = [#] V1 by FUNCT_2:def 1;

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

let x be object ; :: thesis: ( x in dom (L * (f * g)) implies (L * (f * g)) . x = ((L * f) * g) . x )
assume x in dom (L * (f * g)) ; :: thesis: (L * (f * g)) . x = ((L * f) * 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 A2, FUNCT_1:13
.= (L * f) . (g . v) by MATRLIN:def 4
.= ((L * f) * g) . x by A1, FUNCT_1:12 ; :: thesis: verum

end;

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