let A, B be non empty set ; for f being Function of A,B
for C being Subset of A
for v being Element of B holds f +* (C --> v) is Function of A,B
let f be Function of A,B; for C being Subset of A
for v being Element of B holds f +* (C --> v) is Function of A,B
let C be Subset of A; for v being Element of B holds f +* (C --> v) is Function of A,B
let v be Element of B; f +* (C --> v) is Function of A,B
A1:
dom f = A
by FUNCT_2:def 1;
( rng f c= B & rng (C --> v) c= {v} )
by FUNCOP_1:13, RELAT_1:def 19;
then A2:
(rng f) \/ (rng (C --> v)) c= B \/ {v}
by XBOOLE_1:13;
rng (f +* (C --> v)) c= (rng f) \/ (rng (C --> v))
by FUNCT_4:17;
then
rng (f +* (C --> v)) c= B \/ {v}
by A2, XBOOLE_1:1;
then A3:
rng (f +* (C --> v)) c= B
by ZFMISC_1:40;
dom (f +* (C --> v)) =
(dom f) \/ (dom (C --> v))
by FUNCT_4:def 1
.=
([#] A) \/ C
by A1, FUNCOP_1:13
.=
A
by SUBSET_1:11
;
hence
f +* (C --> v) is Function of A,B
by A3, FUNCT_2:def 1, RELSET_1:4; verum