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