let seq, seq1 be Real_Sequence; :: thesis: ( seq is non-increasing & seq1 is subsequence of seq implies seq1 is non-increasing )
assume that
A1: seq is non-increasing and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is non-increasing
let n be Nat; :: according to SEQM_3:def 9 :: 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 + 1)) <= seq . (Nseq . n) by A1, Th8;
then (seq * Nseq) . (n + 1) <= seq . (Nseq . n) by FUNCT_2:15;
hence seq1 . n >= seq1 . (n + 1) by A3, FUNCT_2:15, A4; :: thesis: verum