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

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

let x be VECTOR of X; :: thesis: ((id the carrier of X) * f) . x = f . x
thus ((id the carrier of X) * f) . x = (ii * f) . x
.= ii . (f . x) by Th4
.= 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
.= f . (ii . x) by Th4
.= f . x ; :: thesis: verum

end;

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