let i be Nat; :: thesis: for D being non empty set
for z being Element of i -tuples_on D
for f being Permutation of (Seg i) holds z * f is Element of i -tuples_on D
let D be non empty set ; :: thesis: for z being Element of i -tuples_on D
for f being Permutation of (Seg i) holds z * f is Element of i -tuples_on D
let z be Element of i -tuples_on D; :: thesis: for f being Permutation of (Seg i) holds z * f is Element of i -tuples_on D
let f be Permutation of (Seg i); :: thesis: z * f is Element of i -tuples_on D
rng f = Seg i by FUNCT_2:def 3;
hence z * f is Element of i -tuples_on D by Th134; :: thesis: verum