let X be ComplexNormSpace; :: thesis: id the carrier of X is bounded LinearOperator of X,X

A1: now

let v, w be VECTOR of X; :: thesis: (id the carrier of X) . (v + w) = ((id the carrier of X) . v) + ((id the carrier of X) . w)
thus (id the carrier of X) . (v + w) = v + w by FUNCT_1:35
.= ((id the carrier of X) . v) + w by FUNCT_1:35
.= ((id the carrier of X) . v) + ((id the carrier of X) . w) by FUNCT_1:35 ; :: thesis: verum

end;

A2: now

let v be VECTOR of X; :: thesis: for z being Complex holds (id the carrier of X) . (z * v) = z * ((id the carrier of X) . v)
let z be Complex; :: thesis: (id the carrier of X) . (z * v) = z * ((id the carrier of X) . v)
thus (id the carrier of X) . (z * v) = z * v by FUNCT_1:35
.= z * ((id the carrier of X) . v) by FUNCT_1:35 ; :: thesis: verum

end;

for v being VECTOR of X holds ||.((id the carrier of X) . v).|| <= 1 * ||.v.|| by FUNCT_1:35;
hence id the carrier of X is bounded LinearOperator of X,X by A1, A2, CLOPBAN1:def 4, CLOPBAN1:def 7, GRCAT_1:def 13; :: thesis: verum