theorem Th56: :: NDIFF13:55

for S, E, F being RealNormSpace
for i being Nat holds CTP (S,(diff_SP (i,S,E)),(diff_SP (i,S,F))) is Lipschitzian LinearOperator of [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (i,S,E)),(diff_SP (i,S,F)):]))