theorem :: NORMSP_1:12

for f being Function
for RNS being non empty 1-sorted
for x being Element of RNS holds
( f is sequence of RNS iff ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) ) )