let X, Y, Z be RealNormSpace; for g being Lipschitzian LinearOperator of X,Y
for f being Lipschitzian LinearOperator of Y,Z
for h being Lipschitzian LinearOperator of X,Z holds
( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
let g be Lipschitzian LinearOperator of X,Y; for f being Lipschitzian LinearOperator of Y,Z
for h being Lipschitzian LinearOperator of X,Z holds
( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
let f be Lipschitzian LinearOperator of Y,Z; for h being Lipschitzian LinearOperator of X,Z holds
( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
let h be Lipschitzian LinearOperator of X,Z; ( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
now ( ( for x being VECTOR of X holds h . x = f . (g . x) ) implies h = f * g )end;
hence
( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
by FUNCT_2:15; verum