theorem Th24: :: NDIFF14:24

for S being RealNormSpace-Sequence
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 ) )