:: deftheorem Def9 defines # MESFUN7C:def 9 :
for X being non empty set
for H being Functional_Sequence of X,COMPLEX
for x being Element of X
for b₄ being Complex_Sequence holds
( b₄ = H # x iff for n being Nat holds b₄ . n = (H . n) . x );