for i being natural Number
for D being non empty set
for z being Tuple of i,D
for f being Permutation of (Seg i) holds z * f is Tuple of i,D