let S be RealNormSpace-Sequence; :: thesis: for s being set holds
( proj (In (s,(dom S))) is Lipschitzian LinearOperator of (product S),(S . (In (s,(dom S)))) & ex LP being Point of (R_NormSpace_of_BoundedLinearOperators ((product S),(S . (In (s,(dom S)))))) st
( LP = proj (In (s,(dom S))) & ||.LP.|| <= 1 ) )
let s be set ; :: thesis: ( proj (In (s,(dom S))) is Lipschitzian LinearOperator of (product S),(S . (In (s,(dom S)))) & ex LP being Point of (R_NormSpace_of_BoundedLinearOperators ((product S),(S . (In (s,(dom S)))))) st
( LP = proj (In (s,(dom S))) & ||.LP.|| <= 1 ) )
set L1 = proj (In (s,(dom S)));
set F = S . (In (s,(dom S)));
set E = product S;
A1: proj (In (s,(dom S))) is additive by NDIFF_5:35;
for x being VECTOR of (product S)
for a being Real holds (proj (In (s,(dom S)))) . (a * x) = a * ((proj (In (s,(dom S)))) . x) by NDIFF_5:40;
then reconsider L1 = proj (In (s,(dom S))) as LinearOperator of (product S),(S . (In (s,(dom S)))) by A1, LOPBAN_1:def 5;
set K = 1;
for x being VECTOR of (product S) holds ||.(L1 . x).|| <= 1 * ||.x.|| by NDIFF_5:31;
hence A3: proj (In (s,(dom S))) is Lipschitzian LinearOperator of (product S),(S . (In (s,(dom S)))) by LOPBAN_1:def 8; :: thesis: ex LP being Point of (R_NormSpace_of_BoundedLinearOperators ((product S),(S . (In (s,(dom S)))))) st
( LP = proj (In (s,(dom S))) & ||.LP.|| <= 1 )
then reconsider LP = L1 as Point of (R_NormSpace_of_BoundedLinearOperators ((product S),(S . (In (s,(dom S)))))) by LOPBAN_1:def 9;
take LP ; :: thesis: ( LP = proj (In (s,(dom S))) & ||.LP.|| <= 1 )
thus LP = proj (In (s,(dom S))) ; :: thesis: ||.LP.|| <= 1
A5: for x being Real st x in PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))) holds
x <= 1

proof

let x be Real; :: thesis: ( x in PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))) implies x <= 1 )
assume x in PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))) ; :: thesis: x <= 1
then consider y being VECTOR of (product S) such that
A6: ( x = ||.((modetrans (LP,(product S),(S . (In (s,(dom S)))))) . y).|| & ||.y.|| <= 1 ) ;
A7: ||.(L1 . y).|| <= 1 * ||.y.|| by NDIFF_5:31;
LP = modetrans (LP,(product S),(S . (In (s,(dom S))))) by A3, LOPBAN_1:29;
hence x <= 1 by A6, A7, XXREAL_0:2; :: thesis: verum

end;

reconsider LP0 = LP as Element of BoundedLinearOperators ((product S),(S . (In (s,(dom S))))) ;
A8: PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))) is bounded_above

proof

for x being ExtReal st x in PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))) holds
x <= 1 by A5;
then 1 is UpperBound of PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))) by XXREAL_2:def 1;
hence PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))) is bounded_above ; :: thesis: verum

end;

now :: thesis: not upper_bound (PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S))))))) > 1

assume A9: upper_bound (PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S))))))) > 1 ; :: thesis: contradiction
set dif = (upper_bound (PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))))) - 1;
(upper_bound (PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))))) - 1 > 0 by A9, XREAL_1:50;
then ex w being Real st
( w in PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))) & (upper_bound (PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))))) - ((upper_bound (PreNorms (modetrans (LP,(product S),(S . (In (s,(dom S)))))))) - 1) < w ) by A8, SEQ_4:def 1;
hence contradiction by A5; :: thesis: verum

end;

hence ||.LP.|| <= 1 by LOPBAN_1:def 13; :: thesis: verum