let U be Universe; :: thesis: for X being set
for n being non zero Nat st n -tuples_on {X} is Element of U holds
X is Element of U
let X be set ; :: thesis: for n being non zero Nat st n -tuples_on {X} is Element of U holds
X is Element of U
let n be non zero Nat; :: thesis: ( n -tuples_on {X} is Element of U implies X is Element of U )
assume n -tuples_on {X} is Element of U ; :: thesis: X is Element of U
then Funcs ((Seg n),{X}) is Element of U by FINSEQ_2:93;
hence X is Element of U by Th19; :: thesis: verum