let i be Nat; :: thesis: for D, D9 being non empty set
for z being Tuple of i,D
for f being Function of D,D9 holds f * z is Element of i -tuples_on D9
let D, D9 be non empty set ; :: thesis: for z being Tuple of i,D
for f being Function of D,D9 holds f * z is Element of i -tuples_on D9
let z be Tuple of i,D; :: thesis: for f being Function of D,D9 holds f * z is Element of i -tuples_on D9
let f be Function of D,D9; :: thesis: f * z is Element of i -tuples_on D9
reconsider s = f * z as FinSequence of D9 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 D9 by Th110; :: thesis: verum