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