let X be set ; :: thesis: for y being object
for f being PartFunc of X,{y}
for g being Function of X,{y} holds TotFuncs f = {g}
let y be object ; :: 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 object holds
( h in TotFuncs f iff h = g )

proof

let h be object ; :: 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 Th81;
hence h = g by Th50; :: thesis: verum

end;

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

end;

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