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