let i be Nat; :: thesis: for D being non empty set
for D' being non empty Subset of D
for z being Element of i -tuples_on D' holds z is Element of i -tuples_on D
let D be non empty set ; :: thesis: for D' being non empty Subset of D
for z being Element of i -tuples_on D' holds z is Element of i -tuples_on D
let D' be non empty Subset of D; :: thesis: for z being Element of i -tuples_on D' holds z is Element of i -tuples_on D
let z be Element of i -tuples_on D'; :: thesis: z is Element of i -tuples_on D
( z is FinSequence of D & len z = i ) by Th27, FINSEQ_1:def 18;
hence z is Element of i -tuples_on D by Th110; :: thesis: verum