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

proof

A2: 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;

now

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

end;

hence id the carrier of X is LinearOperator of X,X by A2, LOPBAN_1:def 5, LOPBAN_1:def 6; :: 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, LOPBAN_1:def 9; :: thesis: verum