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