consider f being Function of VAR ,D;
f in VAL D by Def2;
hence not VAL D is empty ; :: thesis: verum