theorem :: NDIFF12:17

for E, F being RealNormSpace
for i being Nat holds 0. (diff_SP ((i + 1),E,F)) = ([#] E) --> (0. (diff_SP (i,E,F)))