theorem :: TBSP_1:4

for N being non empty MetrStruct
for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) )