for S, T being RealNormSpace
for i being Nat ex H being RealNormSpace st
( H = (diff_SP (S,T)) . i & (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H) )