let seq1, seq2 be ExtREAL_sequence; :: thesis: for k being Nat st ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k )
let k be Nat; :: thesis: ( ( for n being Nat holds seq1 . n <= seq2 . n ) implies ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k ) )
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
assume A1: for n being Nat holds seq1 . n <= seq2 . n ; :: thesis: ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k )
A2: now :: thesis: for n being Nat holds (seq1 ^\ k1) . n <= (seq2 ^\ k1) . n
let n be Nat; :: thesis: (seq1 ^\ k1) . n <= (seq2 ^\ k1) . n
A3: (seq2 ^\ k1) . n = seq2 . (n + k) by NAT_1:def 3;
(seq1 ^\ k1) . n = seq1 . (n + k) by NAT_1:def 3;
hence (seq1 ^\ k1) . n <= (seq2 ^\ k1) . n by A1, A3; :: thesis: verum
end;
then sup (seq1 ^\ k1) <= sup (seq2 ^\ k1) by MESFUNC5:55;
then A4: (superior_realsequence seq1) . k <= sup (seq2 ^\ k1) by RINFSUP2:27;
inf (seq1 ^\ k1) <= inf (seq2 ^\ k1) by A2, Th1;
then (inferior_realsequence seq1) . k <= inf (seq2 ^\ k1) by RINFSUP2:27;
hence ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k ) by A4, RINFSUP2:27; :: thesis: verum