:: deftheorem Def3 defines * NDIFF_1:def 3 :
for RNS being RealLinearSpace
for z being Point of RNS
for a being Real_Sequence
for b₄ being sequence of RNS holds
( b₄ = a * z iff for n being Nat holds b₄ . n = (a . n) * z );