theorem Th19: :: NDIFF12:19

for E, F being RealNormSpace
for L being Lipschitzian LinearOperator of E,F
for i being Nat holds
( diff (L,(i + 1),([#] E)) is_differentiable_on [#] E & (diff (L,(i + 1),([#] E))) `| ([#] E) = ([#] E) --> (0. (diff_SP ((i + 2),E,F))) & (diff (L,(i + 1),([#] E))) `| ([#] E) is_continuous_on [#] E )