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

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