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 (inferior_realsequence f) . n = inf (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; :: thesis: for n being Element of NAT holds (inferior_realsequence f) . n = inf (f ^\ n)
let n be Element of NAT ; :: thesis: (inferior_realsequence f) . n = inf (f ^\ n)
reconsider g = f as Function of NAT,(PFuncs (X,ExtREAL)) ;
dom (inf (f ^\ n)) = dom ((f ^\ n) . 0) by Def3;
then dom (inf (f ^\ n)) = dom (g . (n + 0)) by NAT_1:def 3;
then A1: dom (inf (f ^\ n)) = dom (f . 0) by Def2;
A2: dom ((inferior_realsequence f) . n) = dom (f . 0) by Def5;

now

let x be Element of X; :: thesis: ( x in dom (inf (f ^\ n)) implies (inf (f ^\ n)) . x = ((inferior_realsequence f) . n) . x )
assume A3: x in dom (inf (f ^\ n)) ; :: thesis: (inf (f ^\ n)) . x = ((inferior_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:63;
then A4: (inf (f ^\ n)) . x = inf ((f # x) ^\ n) by A3, Def3;
((inferior_realsequence f) . n) . x = (inferior_realsequence (f # x)) . n by A2, A1, A3, Def5;
hence (inf (f ^\ n)) . x = ((inferior_realsequence f) . n) . x by A4, RINFSUP2:27; :: thesis: verum

end;

hence (inferior_realsequence f) . n = inf (f ^\ n) by A2, A1, PARTFUN1:5; :: thesis: verum