let X be RealNormSpace; :: thesis: for f, g, h being Lipschitzian LinearOperator of X,X holds f * (g * h) = (f * g) * h
let f, g, h be Lipschitzian LinearOperator of X,X; :: thesis: f * (g * h) = (f * g) * h

now :: thesis: for x being VECTOR of X holds (f * (g * h)) . x = ((f * g) * h) . x

let x be VECTOR of X; :: thesis: (f * (g * h)) . x = ((f * g) * h) . x
thus (f * (g * h)) . x = f . ((g * h) . x) by Th4
.= f . (g . (h . x)) by Th4
.= (f * g) . (h . x) by FUNCT_2:15
.= ((f * g) * h) . x by Th4 ; :: thesis: verum

end;

hence f * (g * h) = (f * g) * h by FUNCT_2:63; :: thesis: verum