:: deftheorem Def1 defines (#) SEQFUNC2:def 1 :
for D being non empty set
for Y being non empty NORMSTR
for H being Functional_Sequence of D, the carrier of Y
for r being Real
for b₅ being Functional_Sequence of D, the carrier of Y holds
( b₅ = r (#) H iff for n being Nat holds b₅ . n = r (#) (H . n) );