theorem Th18: :: NDIFF12:18

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