theorem Th3: :: DIST_2:3

for S being non empty finite set
for x being Element of S holds
( x in rng (canFS S) & ex n being Nat st
( n in dom (canFS S) & x = (canFS S) . n & n in Seg (card S) ) )