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

thus TotFuncs f c= Funcs X,Y :: thesis: verum

proof

let g be set ; :: 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 Th158;
hence g in Funcs X,Y by A1, Th11; :: thesis: verum

end;

end;

end;