theorem Th16: :: NDIFF12:16

for E, F being RealNormSpace
for L being Lipschitzian LinearOperator of E,F holds
( (diff (L,([#] E))) . 0 = L & (diff (L,([#] E))) . 1 = ([#] E) --> L & (diff (L,([#] E))) . 2 = ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) & (diff (L,([#] E))) . 3 = ([#] E) --> (([#] E) --> (([#] E) --> (([#] E) --> (0. F)))) )