for S, T being RealNormSpace holds
( (diff_SP (S,T)) . 0 = T & (diff_SP (S,T)) . 1 = R_NormSpace_of_BoundedLinearOperators (S,T) & (diff_SP (S,T)) . 2 = R_NormSpace_of_BoundedLinearOperators (S,(R_NormSpace_of_BoundedLinearOperators (S,T))) )