:: deftheorem Def1 defines (#) SEQFUNC:def 1 :
for D being non empty set
for H being Functional_Sequence of D,REAL
for r being Real
for b₄ being Functional_Sequence of D,REAL holds
( b₄ = r (#) H iff for n being Nat holds b₄ . n = r (#) (H . n) );