let X be RealNormSpace; :: thesis: id the carrier of X is Lipschitzian LinearOperator of X,X
A1: for v, w being VECTOR of X holds (id the carrier of X) . (v + w) = ((id the carrier of X) . v) + ((id the carrier of X) . w) ;
A2: for v being VECTOR of X
for a being Real holds (id the carrier of X) . (a * v) = a * ((id the carrier of X) . v) ;
for v being VECTOR of X holds ||.((id the carrier of X) . v).|| <= 1 * ||.v.|| ;
hence id the carrier of X is Lipschitzian LinearOperator of X,X by A1, A2, LOPBAN_1:def 5, LOPBAN_1:def 8, VECTSP_1:def 20; :: thesis: verum