theorem Th8: :: MESFUNC8:8

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