dom f = NAT by FUNCT_2:def 1;
then f . 1 = f . 0 by FUNCT_1:def 10;
hence difference f is zero ; :: thesis: verum