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) )

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

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

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

let 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;

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

end;

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