let i be Nat; :: thesis: for D being non empty set
for D' being non empty Subset of
for z being Tuple of i,D' holds z is Element of i -tuples_on D
let D be non empty set ; :: thesis: for D' being non empty Subset of
for z being Tuple of i,D' holds z is Element of i -tuples_on D
let D' be non empty Subset of ; :: thesis: for z being Tuple of i,D' holds z is Element of i -tuples_on D
let z be Tuple of i,D'; :: thesis: z is Element of i -tuples_on D
z is Tuple of i,D by Th27;
hence z is Element of i -tuples_on D by Lemat; :: thesis: verum