ex H being RealNormSpace st
( H = (diff_SP (S,T)) . i & (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H) ) by Th9;
hence (diff_SP (S,T)) . i is RealNormSpace ; :: thesis: verum