let X, y be set ; :: thesis: for f being PartFunc of X,{y}
for g being Function of X,{y} holds TotFuncs f = {g}
let f be PartFunc of X,{y}; :: thesis: for g being Function of X,{y} holds TotFuncs f = {g}
let g be Function of X,{y}; :: thesis: TotFuncs f = {g}
for h being set holds
( h in TotFuncs f iff h = g )

proof

let h be set ; :: thesis: ( h in TotFuncs f iff h = g )
thus ( h in TotFuncs f implies h = g ) :: thesis: ( h = g implies h in TotFuncs f )

proof

assume h in TotFuncs f ; :: thesis: h = g
then h is Function of X,{y} by Th158;
hence h = g by Th66; :: thesis: verum

end;

f tolerates g by PARTFUN1:143;
hence ( h = g implies h in TotFuncs f ) by PARTFUN1:def 7; :: thesis: verum

end;

hence TotFuncs f = {g} by TARSKI:def 1; :: thesis: verum