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 )

( 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;thus ((id the carrier of X) * f) . x = (ii * f) . x

.= ii . (f . x) by Th4

.= f . x ; :: thesis: verum

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

hence
( f * (id the carrier of X) = f & (id the carrier of X) * f = f )
by A1, FUNCT_2:63; :: thesis: verumlet 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;thus (f * (id the carrier of X)) . x = (f * ii) . x

.= f . (ii . x) by Th4

.= f . x ; :: thesis: verum