:: deftheorem Def13 defines # MESFUNC5:def 13 :
for X being non empty set
for H being Functional_Sequence of X,ExtREAL
for x being Element of X
for b₄ being ExtREAL_sequence holds
( b₄ = H # x iff for n being Nat holds b₄ . n = (H . n) . x );