let i be natural Number ; :: thesis: for D being non empty set
for D9 being non empty Subset of D
for z being Tuple of i,D9 holds z is Element of i -tuples_on D
let D be non empty set ; :: thesis: for D9 being non empty Subset of D
for z being Tuple of i,D9 holds z is Element of i -tuples_on D
let D9 be non empty Subset of D; :: thesis: for z being Tuple of i,D9 holds z is Element of i -tuples_on D
let z be Tuple of i,D9; :: thesis: z is Element of i -tuples_on D
z is Tuple of i,D by Th22;
hence z is Element of i -tuples_on D by Lm6; :: thesis: verum