let X be non empty set ; :: thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n)
let n be Nat; :: thesis: (inferior_realsequence f) . n = inf (f ^\ n)
n in NAT by ORDINAL1:def 12;
then (inferior_realsequence (R_EAL f)) . n = inf ((R_EAL f) ^\ n) by MESFUNC8:8;
hence (inferior_realsequence f) . n = inf (f ^\ n) ; :: thesis: verum