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

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 LOPBAN_1:27;

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 LOPBAN_1:30; :: thesis: verum

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

ii . v = v
;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;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

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 LOPBAN_1:27;

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 LOPBAN_1:30; :: thesis: verum