let n be non zero Nat; :: thesis: odd-seq n is increasing
set F = odd-seq n;
for x1, x2 being Nat st x1 in dom (odd-seq n) & x2 in dom (odd-seq n) & x1 < x2 holds
(odd-seq n) . x1 < (odd-seq n) . x2

proof

let x1, x2 be Nat; :: thesis: ( x1 in dom (odd-seq n) & x2 in dom (odd-seq n) & x1 < x2 implies (odd-seq n) . x1 < (odd-seq n) . x2 )
assume A1: ( x1 in dom (odd-seq n) & x2 in dom (odd-seq n) & x1 < x2 ) ; :: thesis: (odd-seq n) . x1 < (odd-seq n) . x2
then A2: ( (odd-seq n) . x1 = (2 * x1) - 1 & (odd-seq n) . x2 = (2 * x2) - 1 ) by Th2;
2 * x1 < 2 * x2 by A1, XREAL_1:68;
hence (odd-seq n) . x1 < (odd-seq n) . x2 by A2, XREAL_1:8; :: thesis: verum

end;

hence odd-seq n is increasing by SEQM_3:def 1; :: thesis: verum