theorem Th5: :: MESFUN7C:5

for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )