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