theorem Th56: :: FINSEQ_1:56

for X being set st X is finite holds
ex n being Nat st X, Seg n are_equipotent