let n be Nat; :: thesis: for r being Real
for seq being Real_Sequence st seq is bounded_below holds
( ( for k being Nat holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
let r be Real; :: thesis: for seq being Real_Sequence st seq is bounded_below holds
( ( for k being Nat holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies ( ( for k being Nat holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n ) )
reconsider Y1 = { (seq . k) where k is Nat : n <= k } as Subset of REAL by Th29;
set seq1 = seq ^\ n;
assume seq is bounded_below ; :: thesis: ( ( for k being Nat holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
then A1: seq ^\ n is bounded_below by SEQM_3:28;
A2: rng (seq ^\ n) = Y1 by Th30;
thus ( ( for k being Nat holds r <= seq . (n + k) ) implies r <= (inferior_realsequence seq) . n ) :: thesis: ( r <= (inferior_realsequence seq) . n implies for k being Nat holds r <= seq . (n + k) )

proof

assume A3: for k being Nat holds r <= seq . (n + k) ; :: thesis: r <= (inferior_realsequence seq) . n

now :: thesis: for n1 being Nat holds r <= (seq ^\ n) . n1

let n1 be Nat; :: thesis: r <= (seq ^\ n) . n1
n1 in NAT by ORDINAL1:def 12;
then (seq ^\ n) . n1 in rng (seq ^\ n) by FUNCT_2:4;
then consider r1 being Real such that
A4: (seq ^\ n) . n1 = r1 and
A5: r1 in Y1 by A2;
consider k1 being Nat such that
A6: r1 = seq . k1 and
A7: n <= k1 by A5;
consider k2 being Nat such that
A8: k1 = n + k2 by A7, NAT_1:10;
thus r <= (seq ^\ n) . n1 by A3, A4, A6, A8; :: thesis: verum

end;

then r <= lower_bound (seq ^\ n) by Th10;
then r <= lower_bound Y1 by Th30;
hence r <= (inferior_realsequence seq) . n by Def4; :: thesis: verum

end;

assume r <= (inferior_realsequence seq) . n ; :: thesis: for k being Nat holds r <= seq . (n + k)
then r <= lower_bound Y1 by Def4;
then A9: r <= lower_bound (seq ^\ n) by Th30;

now :: thesis: for m1 being Nat holds r <= seq . (n + m1)

let m1 be Nat; :: thesis: r <= seq . (n + m1)
n <= n + m1 by NAT_1:11;
then seq . (n + m1) in Y1 ;
then seq . (n + m1) in rng (seq ^\ n) by Th30;
then ex k being object st
( k in dom (seq ^\ n) & (seq ^\ n) . k = seq . (n + m1) ) by FUNCT_1:def 3;
hence r <= seq . (n + m1) by A1, A9, Th10; :: thesis: verum

end;

hence for k being Nat holds r <= seq . (n + k) ; :: thesis: verum