let x be set ; :: according to FINSEQ_1:def 18 :: thesis: ( not x in n -tuples_on D or x is set )
assume x in n -tuples_on D ; :: thesis: x is set
then ex s being Element of D * st
( x = s & len s = n ) ;
hence x is set ; :: thesis: verum