:: deftheorem Def6 defines superior_realsequence MESFUNC8:def 6 :
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₃ = superior_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 = (superior_realsequence (f # x)) . n ) ) );