let a be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds a . n = (2 * n) + 1 ) implies a is V35() sequence of NAT )
assume A1: for n being Element of NAT holds a . n = (2 * n) + 1 ; :: 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) + 1) + 0 < ((2 * n) + 1) + 2 by XREAL_1:10;
((2 * n) + 1) + 2 = (2 * (n + 1)) + 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 dom a implies a . x in NAT )
assume x in dom a ; :: thesis: a . x in NAT
then reconsider n = x as Element of NAT ;
a . n = (2 * n) + 1 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