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