let x, y, X, Y be set ; :: thesis: for f being PartFunc of X,Y st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y
let f be PartFunc of X,Y; :: thesis: ( x in X & y in Y implies f +* (x .--> y) is PartFunc of X,Y )
assume A1: ( x in X & y in Y ) ; :: thesis: f +* (x .--> y) is PartFunc of X,Y
set F = f +* (x .--> y);
A2: rng (f +* (x .--> y)) c= (rng f) \/ (rng (x .--> y)) by FUNCT_4:18;

now

let z be set ; :: thesis: ( z in rng (f +* (x .--> y)) implies z in Y )
assume A3: z in rng (f +* (x .--> y)) ; :: thesis: z in Y

now

per cases ( z in rng f or z in rng (x .--> y) ) by A2, A3, XBOOLE_0:def 3;

suppose z in rng f ; :: thesis: z in Y

hence z in Y ; :: thesis: verum

end;

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

then z in {y} by FUNCOP_1:14;
hence z in Y by A1, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence z in Y ; :: thesis: verum

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:11;

now

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

now

per cases ( z in dom f or z in dom (x .--> y) ) by A4, XBOOLE_0:def 3;

suppose z in dom f ; :: thesis: z in X

hence z in X ; :: thesis: verum

end;

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

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

end;

end;

end;

hence z in X ; :: thesis: verum

end;

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