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 Lipschitzian LinearOperator of X,X by Th3;
A2: now :: thesis: for r being Real st r in PreNorms ii holds
r <= 1
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 ; :: thesis: verum
end;
ii . v = v ;
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:26;
then A4: 1 <= upper_bound (PreNorms ii) by A3, SEQ_4:def 1;
( ( for s being Real st s in PreNorms ii holds
s <= 1 ) implies upper_bound (PreNorms ii) <= 1 ) by SEQ_4:45;
then upper_bound (PreNorms ii) = 1 by A2, A4, XXREAL_0:1;
hence (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1 by CLOPBAN1:29; :: thesis: verum