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)
A0: n in NAT by ORDINAL1:def 13;
(superior_realsequence (R_EAL f)) . n = sup ((R_EAL f) ^\ n) by A0, MESFUNC8:9;
hence (superior_realsequence f) . n = sup (f ^\ n) by LEM5; :: thesis: verum