theorem Th36: :: RINFSUP1:36

for n being Nat
for seq being Real_Sequence holds (inferior_realsequence seq) . n = lower_bound (seq ^\ n)