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

proof

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

end;

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