theorem Th1: :: CARDFIL3:2

for I, J being set st J in Fin I holds
ex p being FinSequence of I st
( J = rng p & p is one-to-one )