:: deftheorem Def5 defines inferior_realsequence MESFUNC8:def 5 :
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b₃ being with_the_same_dom Functional_Sequence of X,ExtREAL holds
( b₃ = inferior_realsequence f iff for n being Nat holds
( dom (b₃ . n) = dom (f . 0) & ( for x being Element of X st x in dom (b₃ . n) holds
(b₃ . n) . x = (inferior_realsequence (f # x)) . n ) ) );