:: deftheorem Def14 defines - DUALSP01:def 8 :
for S being Real_Sequence
for x being Real
for b₃ being Real_Sequence holds
( b₃ = S - x iff for n being Nat holds b₃ . n = (S . n) - x );