let UN be Universe; :: thesis: for X being set st X in UN holds
for n being Nat holds n -tuples_on X in UN
let X be set ; :: thesis: ( X in UN implies for n being Nat holds n -tuples_on X in UN )
assume A1: X in UN ; :: thesis: for n being Nat holds n -tuples_on X in UN
let n be Nat; :: thesis: n -tuples_on X in UN
Seg n in UN by Th57;
then Funcs ((Seg n),X) in UN by A1, CLASSES2:61;
hence n -tuples_on X in UN by FINSEQ_2:93; :: thesis: verum