for S, T being RealNormSpace
for i being Nat holds diff_SP ((i + 1),S,T) = R_NormSpace_of_BoundedLinearOperators (S,(diff_SP (i,S,T)))