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: ii . v = v by FUNCT_1:35;

A3: now

let r be Real; :: thesis: ( r in PreNorms ii implies r <= 1 )
assume A4: r in PreNorms ii ; :: thesis: r <= 1
consider t being VECTOR of X such that
A5: ( r = ||.(ii . t).|| & ||.t.|| <= 1 ) by A4;
thus r <= 1 by A5, FUNCT_1:35; :: thesis: verum

end;

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