let a be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds a . n = 2 * n ) implies a is increasing sequence of NAT )
assume A1: for n being Element of NAT holds a . n = 2 * n ; :: thesis: a is increasing sequence of NAT
A2: a is increasing

proof

let n be Nat; :: according to VALUED_1:def 13 :: thesis: not a . (n + 1) <= a . n
A3: n in NAT by ORDINAL1:def 12;
A4: (2 * n) + 0 < (2 * n) + 2 by XREAL_1:8;
(2 * n) + 2 = 2 * (n + 1)
.= a . (n + 1) by A1 ;
hence a . n < a . (n + 1) by A1, A4, A3; :: thesis: verum

end;

A5: now :: thesis: for x being object st x in NAT holds
a . x in NAT

let x be object ; :: thesis: ( x in NAT implies a . x in NAT )
assume x in NAT ; :: thesis: a . x in NAT
then reconsider n = x as Element of NAT ;
a . n = 2 * n by A1;
hence a . x in NAT ; :: thesis: verum

end;

dom a = NAT by FUNCT_2:def 1;
hence a is increasing sequence of NAT by A2, A5, FUNCT_2:3; :: thesis: verum