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

proof

let n be Element of NAT ; :: according to SEQM_3:def 11 :: thesis: not a . (n + 1) <= a . n
A2: (2 * n) + 0 < (2 * n) + 2 by XREAL_1:10;
(2 * n) + 2 = 2 * (n + 1)
.= a . (n + 1) by A1 ;
hence a . n < a . (n + 1) by A1, A2; :: thesis: verum

end;

B1: now

let x be set ; :: 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;
then a is sequence of NAT by B1, FUNCT_2:5;
hence a is V35() sequence of NAT by X; :: thesis: verum