theorem Th30: :: NDIFF13:29

for E, F being RealNormSpace
for i being Nat holds diff_SP ((i + 1),E,F) = diff_SP (i,E,(R_NormSpace_of_BoundedLinearOperators (E,F)))