let i be Nat; :: thesis: for D, D' being non empty set
for z being Tuple of i,D
for f being Function of D,D' holds f * z is Element of i -tuples_on D'
let D, D' be non empty set ; :: thesis: for z being Tuple of i,D
for f being Function of D,D' holds f * z is Element of i -tuples_on D'
let z be Tuple of i,D; :: thesis: for f being Function of D,D' holds f * z is Element of i -tuples_on D'
let f be Function of D,D'; :: thesis: f * z is Element of i -tuples_on D'
reconsider s = f * z as FinSequence of D' by Th36;
len z = i by FINSEQ_1:def 18;
then len s = i by Th37;
hence f * z is Element of i -tuples_on D' by Th110; :: thesis: verum