len (Rev f) = n by CARD_1:def 7;
hence Rev f is Element of n -tuples_on D by FINSEQ_2:92; :: thesis: verum