let seq, seq1 be Real_Sequence; :: thesis: ( seq is non-decreasing & seq1 is subsequence of seq implies seq1 is non-decreasing )
assume that
A1: seq is non-decreasing and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is non-decreasing
let n be Nat; :: according to SEQM_3:def 8 :: thesis: seq1 . n <= seq1 . (n + 1)
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def 17;
A4: n in NAT by ORDINAL1:def 12;
Nseq . n <= Nseq . (n + 1) by Lm7;
then seq . (Nseq . n) <= seq . (Nseq . (n + 1)) by A1, Th6;
then (seq * Nseq) . n <= seq . (Nseq . (n + 1)) by FUNCT_2:15, A4;
hence seq1 . n <= seq1 . (n + 1) by A3, FUNCT_2:15; :: thesis: verum