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