let i, j be Nat; :: thesis: for D being non empty set
for z being Element of i -tuples_on D
for t being Element of j -tuples_on D holds z ^ t is Element of (i + j) -tuples_on D
let D be non empty set ; :: thesis: for z being Element of i -tuples_on D
for t being Element of j -tuples_on D holds z ^ t is Element of (i + j) -tuples_on D
let z be Element of i -tuples_on D; :: thesis: for t being Element of j -tuples_on D holds z ^ t is Element of (i + j) -tuples_on D
let t be Element of j -tuples_on D; :: thesis: z ^ t is Element of (i + j) -tuples_on D
z ^ t in { (z' ^ t') where z' is Element of i -tuples_on D, t' is Element of j -tuples_on D : verum } ;
hence z ^ t is Element of (i + j) -tuples_on D by Th125; :: thesis: verum