let i be Nat; :: thesis: for D being non empty set
for z being Element of i -tuples_on D
for f being Function of (Seg i),(Seg i) st rng f = 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 Function of (Seg i),(Seg i) st rng f = 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 Function of (Seg i),(Seg i) st rng f = Seg i holds
z * f is Element of i -tuples_on D
let f be Function of (Seg i),(Seg i); :: thesis: ( rng f = Seg i implies z * f is Element of i -tuples_on D )
assume A1: rng f = Seg i ; :: thesis: z * f is Element of i -tuples_on D
A2: len z = i by FINSEQ_1:def 18;
then A3: Seg i = dom z by FINSEQ_1:def 3;
then reconsider t = z * f as FinSequence of D by Th51;
len t = len z by A1, A3, Th46;
hence z * f is Element of i -tuples_on D by A2, Th110; :: thesis: verum