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

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