let X, Y be set ; :: thesis: for f being PartFunc of X,Y holds
( f is total iff TotFuncs f = {f} )
let f be PartFunc of X,Y; :: thesis: ( f is total iff TotFuncs f = {f} )
thus ( f is total implies TotFuncs f = {f} ) :: thesis: ( TotFuncs f = {f} implies f is total )

proof

assume A1: f is total ; :: thesis: TotFuncs f = {f}
for g being object holds
( g in TotFuncs f iff f = g )

proof

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

proof

assume g in TotFuncs f ; :: thesis: f = g
then ex g9 being PartFunc of X,Y st
( g9 = g & g9 is total & f tolerates g9 ) by Def5;
hence f = g by A1, Th66; :: thesis: verum

end;

thus ( f = g implies g in TotFuncs f ) by A1, Def5; :: thesis: verum

end;

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

end;

assume TotFuncs f = {f} ; :: thesis: f is total
then f in TotFuncs f by TARSKI:def 1;
hence f is total by Th70; :: thesis: verum