let i be natural Number ; :: 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 Th30;
len z = i by CARD_1:def 7;
then len s = i by Th31;
hence f * z is Element of i -tuples_on D9 by Th90; :: thesis: verum