for a being Real_Sequence st ( for n being Element of NAT holds a . n = 2 * n ) holds
a is V43() sequence of NAT