theorem Th62: :: CLASSES4:62

for X being non empty set
for x being object st x in X * holds
ex n being Nat st x in n -tuples_on X