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

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

hence
f * (g * h) = (f * g) * h
by FUNCT_2:63; :: thesis: verumlet 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;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