theorem Th20: :: NDIFF12:20

for E, F being RealNormSpace
for L being Lipschitzian LinearOperator of E,F
for i being Nat holds
( diff (L,i,([#] E)) is_differentiable_on [#] E & (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E )