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