let X be non empty set ; :: thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for n being Element of NAT holds (superior_realsequence f) . n = sup (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,ExtREAL ; :: thesis: for n being Element of NAT holds (superior_realsequence f) . n = sup (f ^\ n)
let n be Element of NAT ; :: thesis: (superior_realsequence f) . n = sup (f ^\ n)
reconsider g = f as Function of NAT ,(PFuncs X,ExtREAL ) ;
dom (sup (f ^\ n)) = dom ((f ^\ n) . 0 ) by Def4;
then dom (sup (f ^\ n)) = dom (g . (n + 0 )) by NAT_1:def 3;
then A1: dom (sup (f ^\ n)) = dom (f . 0 ) by Def2;
A2: dom ((superior_realsequence f) . n) = dom (f . 0 ) by Def6;

now

let x be Element of X; :: thesis: ( x in dom (sup (f ^\ n)) implies (sup (f ^\ n)) . x = ((superior_realsequence f) . n) . x )
assume A3: x in dom (sup (f ^\ n)) ; :: thesis: (sup (f ^\ n)) . x = ((superior_realsequence f) . n) . x

now

let k be Element of NAT ; :: thesis: ((f ^\ n) # x) . k = ((f # x) ^\ n) . k
((f ^\ n) # x) . k = ((f ^\ n) . k) . x by MESFUNC5:def 13;
then ((f ^\ n) # x) . k = (g . (n + k)) . x by NAT_1:def 3;
then ((f ^\ n) # x) . k = (f # x) . (n + k) by MESFUNC5:def 13;
hence ((f ^\ n) # x) . k = ((f # x) ^\ n) . k by NAT_1:def 3; :: thesis: verum

end;

then (f ^\ n) # x = (f # x) ^\ n by FUNCT_2:113;
then A4: (sup (f ^\ n)) . x = sup ((f # x) ^\ n) by A3, Def4;
((superior_realsequence f) . n) . x = (superior_realsequence (f # x)) . n by A2, A1, A3, Def6;
hence (sup (f ^\ n)) . x = ((superior_realsequence f) . n) . x by A4, RINFSUP2:27; :: thesis: verum

end;

hence (superior_realsequence f) . n = sup (f ^\ n) by A2, A1, PARTFUN1:34; :: thesis: verum