reconsider x = x as Element of INT by INT_1:def 2;
f . x is Element of D ;
hence f . x is Element of D ; :: thesis: verum