let X, Y, Z be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: 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