let S, T be RealNormSpace; :: thesis: for i being Nat holds diff_SP ((i + 1),S,T) = R_NormSpace_of_BoundedLinearOperators (S,(diff_SP (i,S,T)))
let i be Nat; :: thesis: diff_SP ((i + 1),S,T) = R_NormSpace_of_BoundedLinearOperators (S,(diff_SP (i,S,T)))
set H = diff_SP (i,S,T);
ex H1 being RealNormSpace st
( H1 = (diff_SP (S,T)) . i & (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H1) ) by Th9;
hence diff_SP ((i + 1),S,T) = R_NormSpace_of_BoundedLinearOperators (S,(diff_SP (i,S,T))) ; :: thesis: verum