let X, Y be set ; :: thesis: for f being PartFunc of X,Y holds TotFuncs f c= Funcs (X,Y)
let f be PartFunc of X,Y; :: thesis: TotFuncs f c= Funcs (X,Y)

per cases ( ( Y = {} & X <> {} ) or Y <> {} or X = {} ) ;

suppose ( Y = {} & X <> {} ) ; :: thesis: TotFuncs f c= Funcs (X,Y)

hence TotFuncs f c= Funcs (X,Y) ; :: thesis: verum

end;

suppose A1: ( Y <> {} or X = {} ) ; :: thesis: TotFuncs f c= Funcs (X,Y)

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in TotFuncs f or g in Funcs (X,Y) )
assume g in TotFuncs f ; :: thesis: g in Funcs (X,Y)
then g is Function of X,Y by Th81;
hence g in Funcs (X,Y) by A1, Th8; :: thesis: verum

end;

end;