let X be ComplexNormSpace; :: 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 z being Complex holds (id the carrier of X) . (z * v) = z * ((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, CLOPBAN1:def 3, CLOPBAN1:def 6, VECTSP_1:def 20; :: thesis: verum