for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n)