theorem Th63: :: CLASSES4:63

for X being non empty set ex f being Function st
( dom f = NAT & ( for n being Nat holds f . n = n -tuples_on X ) & union (rng f) = X * )