let A, B be set ; for f being Function
for x being set st A misses B holds
(f +* (A --> x)) .: B = f .: B
let f be Function; for x being set st A misses B holds
(f +* (A --> x)) .: B = f .: B
let x be set ; ( A misses B implies (f +* (A --> x)) .: B = f .: B )
assume that
A1:
A /\ B = {}
and
A2:
(f +* (A --> x)) .: B <> f .: B
; XBOOLE_0:def 7 contradiction
A3:
dom (f +* (A --> x)) = (dom f) \/ (dom (A --> x))
by FUNCT_4:def 1;
A4:
dom (A --> x) = A
by FUNCOP_1:13;
A5:
not for y being object holds
( y in (f +* (A --> x)) .: B iff y in f .: B )
by A2, TARSKI:2;
now ( ( ex y being set st
( y in (f +* (A --> x)) .: B & not y in f .: B ) & contradiction ) or ( ex y being set st
( not y in (f +* (A --> x)) .: B & y in f .: B ) & contradiction ) )per cases
( ex y being set st
( y in (f +* (A --> x)) .: B & not y in f .: B ) or ex y being set st
( not y in (f +* (A --> x)) .: B & y in f .: B ) )
by A5;
case
ex
y being
set st
(
y in (f +* (A --> x)) .: B & not
y in f .: B )
;
contradictionthen consider y being
set such that A6:
y in (f +* (A --> x)) .: B
and A7:
not
y in f .: B
;
consider z being
object such that A8:
z in dom (f +* (A --> x))
and A9:
z in B
and A10:
y = (f +* (A --> x)) . z
by A6, FUNCT_1:def 6;
not
z in A
by A1, A9, XBOOLE_0:def 4;
then
(
z in dom f &
y = f . z )
by A3, A4, A8, A10, FUNCT_4:11, XBOOLE_0:def 3;
hence
contradiction
by A7, A9, FUNCT_1:def 6;
verum end; case
ex
y being
set st
( not
y in (f +* (A --> x)) .: B &
y in f .: B )
;
contradictionthen consider y being
set such that A11:
not
y in (f +* (A --> x)) .: B
and A12:
y in f .: B
;
consider z being
object such that A13:
z in dom f
and A14:
z in B
and A15:
y = f . z
by A12, FUNCT_1:def 6;
not
z in A
by A1, A14, XBOOLE_0:def 4;
then A16:
y = (f +* (A --> x)) . z
by A4, A15, FUNCT_4:11;
z in dom (f +* (A --> x))
by A3, A13, XBOOLE_0:def 3;
hence
contradiction
by A11, A14, A16, FUNCT_1:def 6;
verum end;
hence
contradiction
; verum