for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds (R_EAL f) ^\ n = R_EAL (f ^\ n) ;