theorem :: MESFUN7C:10

for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n) by MESFUNC8:9;