let X, Y be set ; :: thesis: for f being PartFunc of X,Y
for x, y being object 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 object st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y
let x, y be object ; :: 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
A3: {x} c= X by A1, ZFMISC_1:31;
{y} c= Y by A2, ZFMISC_1:31;
then rng (x .--> y) c= Y by FUNCOP_1:8;
then A4: (rng f) \/ (rng (x .--> y)) c= Y by XBOOLE_1:8;
rng (f +* (x .--> y)) c= (rng f) \/ (rng (x .--> y)) by Th17;
then A5: rng (f +* (x .--> y)) c= Y by A4;
dom (f +* (x .--> y)) = (dom f) \/ (dom (x .--> y)) by Def1
.= (dom f) \/ {x} ;
hence f +* (x .--> y) is PartFunc of X,Y by A3, A5, RELSET_1:4, XBOOLE_1:8; :: thesis: verum