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 that
A1: x in X and
A2: y in Y ; :: thesis: f +* (x .--> y) is PartFunc of X,Y
set F = f +* (x .--> y);
A3: rng (f +* (x .--> y)) c= (rng f) \/ (rng (x .--> y)) by FUNCT_4:17;

now :: thesis: for z being object st z in rng (f +* (x .--> y)) holds
z in Y

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

now :: thesis: z in Y

per cases ( z in rng f or z in rng (x .--> y) ) by A3, A4, 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:8;
hence z in Y by A2, 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:4;

now :: thesis: for z being object st z in dom F1 holds
z in X

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

now :: thesis: z in X

per cases ( z in dom f or z in dom (x .--> y) ) by A5, 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} ;
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:7; :: thesis: verum