let x, y, X, Y be set ; :: thesis:
let f be PartFunc of X,Y; :: thesis:
assume that
A1: x in X and
A2: y in Y ; :: thesis:
set F = f +* (x .--> y);
A3: rng (f +* (x .--> y)) c= (rng f) \/ (rng (x .--> y)) by FUNCT_4:17;

now :: thesis:

let z be object ; :: thesis:
assume A4: z in rng (f +* (x .--> y)) ; :: thesis:

now :: thesis:

per cases by A3, A4, XBOOLE_0:def 3;

suppose z in rng f ; :: thesis:

hence z in Y ; :: thesis:

end;

suppose z in rng (x .--> y) ; :: thesis:

then z in {y} by FUNCOP_1:8;
hence z in Y by A2, TARSKI:def 1; :: thesis:

end;

end;

end;

hence z in Y ; :: thesis:

end;

then rng (f +* (x .--> y)) c= Y by TARSKI:def 3;
then reconsider F1 = f +* (x .--> y) as PartFunc of (dom (f +* (x .--> y))),Y by RELSET_1:4;

now :: thesis:

let z be object ; :: thesis:
assume z in dom F1 ; :: thesis:
then A5: z in (dom f) \/ (dom (x .--> y)) by FUNCT_4:def 1;

now :: thesis:

per cases by A5, XBOOLE_0:def 3;

suppose z in dom f ; :: thesis:

hence z in X ; :: thesis:

end;

suppose z in dom (x .--> y) ; :: thesis:

then z in {x} ;
hence z in X by A1, TARSKI:def 1; :: thesis:

end;

end;

end;

hence z in X ; :: thesis:

end;

then dom F1 c= X by TARSKI:def 3;
hence f +* (x .--> y) is PartFunc of X,Y by RELSET_1:7; :: thesis: