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 set holds
( g in TotFuncs f iff f = g )

proof

let g be set ; :: 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 g' being PartFunc of X,Y st
( g' = g & g' is total & f tolerates g' ) by Def7;
hence f = g by A1, Th148; :: thesis: verum

end;

thus ( f = g implies g in TotFuncs f ) by A1, Def7; :: 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 Th169; :: thesis: verum