let n be Element of NAT ; :: thesis: for r being real number
for seq being Real_Sequence st seq is bounded_below holds
( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
let r be real number ; :: thesis: for seq being Real_Sequence st seq is bounded_below holds
( ( for k being Element of 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 Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n ) )
assume A1: seq is bounded_below ; :: thesis: ( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29;
set seq1 = seq ^\ n;
A2: rng (seq ^\ n) = Y1 by Th30;
A3: seq ^\ n is bounded_below by A1, Th27;
thus ( ( for k being Element of NAT holds r <= seq . (n + k) ) implies r <= (inferior_realsequence seq) . n ) :: thesis: ( r <= (inferior_realsequence seq) . n implies for k being Element of NAT holds r <= seq . (n + k) )

proof

assume A4: for k being Element of NAT holds r <= seq . (n + k) ; :: thesis: r <= (inferior_realsequence seq) . n

now

let n1 be Element of NAT ; :: thesis: r <= (seq ^\ n) . n1
(seq ^\ n) . n1 in rng (seq ^\ n) by FUNCT_2:6;
then consider r1 being real number such that
A5: ( (seq ^\ n) . n1 = r1 & r1 in Y1 ) by A2;
consider k1 being Element of NAT such that
A6: ( r1 = seq . k1 & n <= k1 ) by A5;
consider k2 being Nat such that
A7: k1 = n + k2 by A6, NAT_1:10;
k2 in NAT by ORDINAL1:def 13;
hence r <= (seq ^\ n) . n1 by A4, A5, A6, A7; :: thesis: verum

end;

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

end;

assume r <= (inferior_realsequence seq) . n ; :: thesis: for k being Element of NAT holds r <= seq . (n + k)
then r <= inf Y1 by Def4;
then A8: r <= inf (seq ^\ n) by Th30;

now

let m1 be Element of 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 consider k being set such that
A9: ( k in dom (seq ^\ n) & (seq ^\ n) . k = seq . (n + m1) ) by FUNCT_1:def 5;
thus r <= seq . (n + m1) by A3, A8, A9, Th10; :: thesis: verum

end;

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