:: deftheorem Def2 defines (#) NDIFF_1:def 2 :
for RNS being RealLinearSpace
for S being sequence of RNS
for a being Real_Sequence
for b₄ being sequence of RNS holds
( b₄ = a (#) S iff for n being Nat holds b₄ . n = (a . n) * (S . n) );