set F = f +* (x,y);
A1: rng (f +* (x,y)) c= (rng f) \/ {y} by Th99;

per cases ( B is empty or not B is empty ) ;

suppose B is empty ; :: thesis: f +* (x,y) is Function of A,B

then dom f is empty ;
hence f +* (x,y) is Function of A,B by Def2; :: thesis: verum

end;

suppose A2: not B is empty ; :: thesis: f +* (x,y) is Function of A,B

then {y} c= B by ZFMISC_1:31;
then (rng f) \/ {y} c= B by XBOOLE_1:8;
then A3: rng (f +* (x,y)) c= B by A1;
dom f = A by A2, FUNCT_2:def 1;
then dom (f +* (x,y)) = A by Th29;
hence f +* (x,y) is Function of A,B by A2, A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;

end;