let X, Y be RealNormSpace; :: thesis: for f being Lipschitzian LinearOperator of X,Y holds
( f * (id the carrier of X) = f & (id the carrier of Y) * f = f )
reconsider ii = id the carrier of X as Lipschitzian LinearOperator of X,X by LOPBAN_2:3;
reconsider jj = id the carrier of Y as Lipschitzian LinearOperator of Y,Y by LOPBAN_2:3;
let f be Lipschitzian LinearOperator of X,Y; :: thesis: ( f * (id the carrier of X) = f & (id the carrier of Y) * f = f )

A1: now :: thesis: for x being VECTOR of X holds ((id the carrier of Y) * f) . x = f . x

let x be VECTOR of X; :: thesis: ((id the carrier of Y) * f) . x = f . x
thus ((id the carrier of Y) * f) . x = jj . (f . x) by FUNCT_2:15
.= f . x ; :: thesis: verum

end;

now :: thesis: for x being VECTOR of X holds (f * (id the carrier of X)) . x = f . x

let x be VECTOR of X; :: thesis: (f * (id the carrier of X)) . x = f . x
thus (f * (id the carrier of X)) . x = f . (ii . x) by FUNCT_2:15
.= f . x ; :: thesis: verum

end;

hence ( f * (id the carrier of X) = f & (id the carrier of Y) * f = f ) by A1, FUNCT_2:63; :: thesis: verum