let i be natural Number ; :: thesis: for D being non empty set
for z being Tuple of i,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 Tuple of i,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 Tuple of i,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 )
A1: len z = i by CARD_1:def 7;
then A2: Seg i = dom z by FINSEQ_1:def 3;
then reconsider t = z * f as FinSequence of D by Th45;
assume rng f = Seg i ; :: thesis: z * f is Element of i -tuples_on D
then len t = len z by A2, Th40;
hence z * f is Element of i -tuples_on D by A1, Th90; :: thesis: verum