for n being Nat
for seq being ExtREAL_sequence holds
( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )