let X be RealNormSpace; :: 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 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;

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, GRCAT_1:def 13, LOPBAN_1:def 6, LOPBAN_1:def 9; :: thesis: verum