let E, F be RealNormSpace; :: thesis: for i being Nat holds 0. (diff_SP ((i + 1),E,F)) = ([#] E) --> (0. (diff_SP (i,E,F)))
let i be Nat; :: thesis: 0. (diff_SP ((i + 1),E,F)) = ([#] E) --> (0. (diff_SP (i,E,F)))
diff_SP ((i + 1),E,F) = R_NormSpace_of_BoundedLinearOperators (E,(diff_SP (i,E,F))) by NDIFF_6:10;
hence 0. (diff_SP ((i + 1),E,F)) = ([#] E) --> (0. (diff_SP (i,E,F))) by LOPBAN_1:31; :: thesis: verum