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

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 Def3; :: 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:37;
then (rng f) \/ {y} c= B by XBOOLE_1:8;
then A3: rng (f +* x,y) c= B by A1, XBOOLE_1:1;
dom f = A by A2, FUNCT_2:def 1;
then dom (f +* x,y) = A by Th32;
hence f +* x,y is Function of A,B by A2, A3, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

end;