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