let X, Y be set ; :: thesis: for f being PartFunc of X,Y
for x, y being set st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y
let f be PartFunc of X,Y; :: thesis: for x, y being set st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y
let x, y be set ; :: thesis: ( x in X & y in Y implies f +* (x .--> y) is PartFunc of X,Y )
assume that
Z1: x in X and
Z2: y in Y ; :: thesis: f +* (x .--> y) is PartFunc of X,Y
C: dom (f +* (x .--> y)) = (dom f) \/ (dom (x .--> y)) by Def1
.= (dom f) \/ {x} by FUNCOP_1:19 ;
B: {x} c= X by Z1, ZFMISC_1:37;
{y} c= Y by Z2, ZFMISC_1:37;
then E: rng (x .--> y) c= Y by FUNCOP_1:14;
D: rng (f +* (x .--> y)) c= (rng f) \/ (rng (x .--> y)) by Th18;
(rng f) \/ (rng (x .--> y)) c= Y by E, XBOOLE_1:8;
then rng (f +* (x .--> y)) c= Y by D, XBOOLE_1:1;
hence f +* (x .--> y) is PartFunc of X,Y by B, C, RELSET_1:11, XBOOLE_1:8; :: thesis: verum