for s being sequence of REAL holds s is Function of NAT,R^1 ;