let seq, seq1 be Real_Sequence; :: thesis: ( seq is decreasing & seq1 is subsequence of seq implies seq1 is decreasing )
assume that
A1: seq is decreasing and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is decreasing
let n be Nat; :: according to SEQM_3:def 7 :: 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, Th4;
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