for seq being ExtREAL_sequence
for j being Element of NAT holds
( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq )