:: deftheorem Def2 defines diff_SP NDIFF_6:def 2 :
for S, T being RealNormSpace
for b₃ being Function holds
( b₃ = diff_SP (S,T) iff ( dom b₃ = NAT & b₃ . 0 = T & ( for i being Nat holds b₃ . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans (b₃ . i))) ) ) );