:: deftheorem Def10 defines # SEQFUNC:def 10 :
for D being non empty set
for H being Functional_Sequence of D,REAL
for x being Element of D
for b₄ being Real_Sequence holds
( b₄ = H # x iff for n being Nat holds b₄ . n = (H . n) . x );