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