F . x in m -tuples_on (n -tuples_on D) ;
hence F . x is Element of m -tuples_on (n -tuples_on D) ; :: thesis: verum