theorem Th23: :: NDIFF14:23

for S being RealNormSpace-Sequence
for s being set holds reproj ((In (s,(dom S))),(0. (product S))) is Lipschitzian LinearOperator of (S . (In (s,(dom S)))),(product S)