let X be non empty set ; :: thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for n being natural number holds (superior_realsequence f) . n = sup (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for n being natural number holds (superior_realsequence f) . n = sup (f ^\ n)
let n be natural number ; :: thesis: (superior_realsequence f) . n = sup (f ^\ n)
n in NAT by ORDINAL1:def 12;
then (superior_realsequence (R_EAL f)) . n = sup ((R_EAL f) ^\ n) by MESFUNC8:9;
hence (superior_realsequence f) . n = sup (f ^\ n) by Th8; :: thesis: verum