assume Z: dom f is trivial ; :: thesis: contradiction

per cases ( dom f is empty or ex x being set st dom f = {x} ) by Z, Def4;

suppose dom f is empty ; :: thesis: contradiction

then f is empty by RELAT_1:64;
hence contradiction ; :: thesis: verum

end;

suppose ex x being set st dom f = {x} ; :: thesis: contradiction

then consider x being set such that
W: dom f = {x} ;
f = {[x,(f . x)]} by W, GRFUNC_1:18;
hence contradiction ; :: thesis: verum

end;

end;