set g = the Element of TotFuncs f;
assume not TotFuncs f is empty ; :: thesis: contradiction
then ex g9 being PartFunc of X,{} st
( g9 = the Element of TotFuncs f & g9 is total & f tolerates g9 ) by Def5;
hence contradiction ; :: thesis: verum