:: deftheorem Def1 defines (#) MESFUN11:def 1 :
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for r being Real
for b₄ being Functional_Sequence of X,ExtREAL holds
( b₄ = r (#) F iff for n being Nat holds b₄ . n = r (#) (F . n) );