let X, Y be set ; 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; 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 ; ( 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
; 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; verum