let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a * b) * f = a * (b * f)
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a * b) * f = a * (b * f)
let f be linear-transformation of V1,V1; :: thesis: for a, b being Scalar of K holds (a * b) * f = a * (b * f)
let a, b be Scalar of K; :: thesis: (a * b) * f = a * (b * f)

A1: now :: thesis: for x being object st x in dom ((a * b) * f) holds
((a * b) * f) . x = (a * (b * f)) . x

let x be object ; :: thesis: ( x in dom ((a * b) * f) implies ((a * b) * f) . x = (a * (b * f)) . x )
assume x in dom ((a * b) * f) ; :: thesis: ((a * b) * f) . x = (a * (b * f)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def 1;
thus ((a * b) * f) . x = (a * b) * (f . v) by MATRLIN:def 4
.= a * (b * (f . v)) by VECTSP_1:def 16
.= a * ((b * f) . v) by MATRLIN:def 4
.= (a * (b * f)) . x by MATRLIN:def 4 ; :: thesis: verum

end;

( dom ((a * b) * f) = [#] V1 & dom (a * (b * f)) = [#] V1 ) by FUNCT_2:def 1;
hence (a * b) * f = a * (b * f) by A1, FUNCT_1:2; :: thesis: verum