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 (inferior_realsequence f) . n = inf (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,REAL ; :: thesis: for n being natural number holds (inferior_realsequence f) . n = inf (f ^\ n)
let n be natural number ; :: thesis: (inferior_realsequence f) . n = inf (f ^\ n)
n in NAT by ORDINAL1:def 13;
then (inferior_realsequence (R_EAL f)) . n = inf ((R_EAL f) ^\ n) by MESFUNC8:8;
hence (inferior_realsequence f) . n = inf (f ^\ n) by LEM5; :: thesis: verum