let i be natural Number ; :: thesis: 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
let D be non empty set ; :: thesis: for z being Tuple of i,D
for f being Permutation of (Seg i) holds z * f is Tuple of i,D
let z be Tuple of i,D; :: thesis: for f being Permutation of (Seg i) holds z * f is Tuple of i,D
let f be Permutation of (Seg i); :: thesis: z * f is Tuple of i,D
rng f = Seg i by FUNCT_2:def 3;
hence z * f is Tuple of i,D by Th112; :: thesis: verum