let X be non trivial ComplexNormSpace; :: thesis: (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1
consider v being VECTOR of X such that
A1: ||.v.|| = 1 by Th17;
reconsider ii = id the carrier of X as bounded LinearOperator of X,X by Th3;

A2: now

let r be Real; :: thesis: ( r in PreNorms ii implies r <= 1 )
assume r in PreNorms ii ; :: thesis: r <= 1
then ex t being VECTOR of X st
( r = ||.(ii . t).|| & ||.t.|| <= 1 ) ;
hence r <= 1 by FUNCT_1:35; :: thesis: verum

end;

ii . v = v by FUNCT_1:35;
then A3: 1 in { ||.(ii . t).|| where t is VECTOR of X : ||.t.|| <= 1 } by A1;
( not PreNorms ii is empty & PreNorms ii is bounded_above ) by CLOPBAN1:30;
then A4: 1 <= upper_bound (PreNorms ii) by A3, SEQ_4:def 4;
( ( for s being real number st s in PreNorms ii holds
s <= 1 ) implies upper_bound (PreNorms ii) <= 1 ) by SEQ_4:62;
then upper_bound (PreNorms ii) = 1 by A2, A4, XXREAL_0:1;
hence (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1 by CLOPBAN1:34; :: thesis: verum