let i be natural Number ; :: thesis: for D being non empty set
for z being set holds
( z is Tuple of i,D iff z in i -tuples_on D )
let D be non empty set ; :: thesis: for z being set holds
( z is Tuple of i,D iff z in i -tuples_on D )
let z be set ; :: thesis: ( z is Tuple of i,D iff z in i -tuples_on D )
thus ( z is Tuple of i,D implies z in i -tuples_on D ) by Lm6; :: thesis: ( z in i -tuples_on D implies z is Tuple of i,D )
assume z in i -tuples_on D ; :: thesis: z is Tuple of i,D
then ex s being Element of D * st
( z = s & len s = i ) ;
hence z is Tuple of i,D by CARD_1:def 7; :: thesis: verum