set D = dom f;
set C = rng f;
( dom f = X & rng f c= X ) by PARTFUN1:def 2;
hence (rng f) \ (dom f) is empty ; :: thesis: verum