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

( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )

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

( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )

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

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

hence
( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
by FUNCT_2:15; :: thesis: verumassume A1:
for x being VECTOR of X holds h . x = f . (g . x)
; :: thesis: h = f * g

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

hence
h = f * g
by FUNCT_2:63; :: thesis: verumlet x be VECTOR of X; :: thesis: (f * g) . x = h . x

thus (f * g) . x = f . (g . x) by FUNCT_2:15

.= h . x by A1 ; :: thesis: verum

end;thus (f * g) . x = f . (g . x) by FUNCT_2:15

.= h . x by A1 ; :: thesis: verum