let X be non empty set ; :: thesis: for f being Functional_Sequence of X,REAL
for n being natural number holds (R_EAL f) ^\ n = R_EAL (f ^\ n)
let f be Functional_Sequence of X,REAL ; :: thesis: for n being natural number holds (R_EAL f) ^\ n = R_EAL (f ^\ n)
let n be natural number ; :: thesis: (R_EAL f) ^\ n = R_EAL (f ^\ n)

now

let m be Element of NAT ; :: thesis: ((R_EAL f) ^\ n) . m = (R_EAL (f ^\ n)) . m
((R_EAL f) ^\ n) . m = R_EAL (f . (n + m)) by NAT_1:def 3;
hence ((R_EAL f) ^\ n) . m = (R_EAL (f ^\ n)) . m by NAT_1:def 3; :: thesis: verum

end;

hence (R_EAL f) ^\ n = R_EAL (f ^\ n) by FUNCT_2:113; :: thesis: verum