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: ( dom ((a * b) * f) = [#] V1 & dom (a * (b * f)) = [#] V1 ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in dom ((a * b) * f) implies ((a * b) * f) . x = (a * (b * f)) . x )
assume A2: x in dom ((a * b) * f) ; :: thesis: ((a * b) * f) . x = (a * (b * f)) . x
reconsider v = x as Element of V1 by A2, FUNCT_2:def 1;
thus ((a * b) * f) . x = (a * b) * (f . v) by MATRLIN:def 6
.= a * (b * (f . v)) by VECTSP_1:def 26
.= a * ((b * f) . v) by MATRLIN:def 6
.= (a * (b * f)) . x by MATRLIN:def 6 ; :: thesis: verum

end;

hence (a * b) * f = a * (b * f) by A1, FUNCT_1:9; :: thesis: verum