theorem :: CARDFIL4:82

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