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

proof

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

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

let n1 be Nat; :: thesis: (seq ^\ n) . n1 <= r
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 (seq ^\ n) . n1 <= r by A3, A4, A6, A8; :: thesis: verum

end;

then upper_bound (seq ^\ n) <= r by Th9;
then upper_bound Y1 <= r by Th30;
hence (superior_realsequence seq) . n <= r by Def5; :: thesis: verum

end;

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

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

let m1 be Nat; :: thesis: seq . (n + m1) <= r
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 seq . (n + m1) <= r by A1, A9, Th9; :: thesis: verum

end;

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