let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y st g in TotFuncs f holds
g is total
let f, g be PartFunc of X,Y; :: thesis: ( g in TotFuncs f implies g is total )
assume g in TotFuncs f ; :: thesis: g is total
then ex g' being PartFunc of X,Y st
( g' = g & g' is total & f tolerates g' ) by Def7;
hence g is total ; :: thesis: verum