theorem Th37: :: RINFSUP1:37

for n being Nat
for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n)