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