theorem :: FINSEQ_1:52

for D being set holds
( D is finite iff ex p being FinSequence st D = rng p )