let X be ComplexNormSpace; :: 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