let S be RealNormSpace-Sequence; :: thesis: for s being set holds reproj ((In (s,(dom S))),(0. (product S))) is Lipschitzian LinearOperator of (S . (In (s,(dom S)))),(product S)
let s be set ; :: thesis: reproj ((In (s,(dom S))),(0. (product S))) is Lipschitzian LinearOperator of (S . (In (s,(dom S)))),(product S)
set L1 = reproj ((In (s,(dom S))),(0. (product S)));
set E = S . (In (s,(dom S)));
set F = product S;
A1: reproj ((In (s,(dom S))),(0. (product S))) is additive by NDIFF_5:34;
for x being VECTOR of (S . (In (s,(dom S))))
for a being Real holds (reproj ((In (s,(dom S))),(0. (product S)))) . (a * x) = a * ((reproj ((In (s,(dom S))),(0. (product S)))) . x) by NDIFF_5:39;
then reconsider L1 = reproj ((In (s,(dom S))),(0. (product S))) as LinearOperator of (S . (In (s,(dom S)))),(product S) by A1, LOPBAN_1:def 5;
set K = 1;
for x being VECTOR of (S . (In (s,(dom S)))) holds ||.(L1 . x).|| <= 1 * ||.x.|| by NDIFF_5:21;
hence reproj ((In (s,(dom S))),(0. (product S))) is Lipschitzian LinearOperator of (S . (In (s,(dom S)))),(product S) by LOPBAN_1:def 8; :: thesis: verum