let A, B be set ; :: thesis: for f being Function
for x being set st A misses B holds
(f +* (A --> x)) .: B = f .: B
let f be Function; :: thesis: for x being set st A misses B holds
(f +* (A --> x)) .: B = f .: B
let x be set ; :: thesis: ( A misses B implies (f +* (A --> x)) .: B = f .: B )
assume that
A1: A /\ B = {} and
A2: (f +* (A --> x)) .: B <> f .: B ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
A3: dom (f +* (A --> x)) = (dom f) \/ (dom (A --> x)) by FUNCT_4:def 1;
A4: dom (A --> x) = A by FUNCOP_1:19;
A5: not for y being set holds
( y in (f +* (A --> x)) .: B iff y in f .: B ) by A2, TARSKI:2;

now

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 ) ; :: thesis: contradiction

then consider y being set such that
A6: y in (f +* (A --> x)) .: B and
A7: not y in f .: B ;
consider z being set 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 12;
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:12, XBOOLE_0:def 3;
hence contradiction by A7, A9, FUNCT_1:def 12; :: thesis: verum

end;

case ex y being set st
( not y in (f +* (A --> x)) .: B & y in f .: B ) ; :: thesis: contradiction

then consider y being set such that
A11: not y in (f +* (A --> x)) .: B and
A12: y in f .: B ;
consider z being set such that
A13: z in dom f and
A14: z in B and
A15: y = f . z by A12, FUNCT_1:def 12;
not z in A by A1, A14, XBOOLE_0:def 4;
then A16: y = (f +* (A --> x)) . z by A4, A15, FUNCT_4:12;
z in dom (f +* (A --> x)) by A3, A13, XBOOLE_0:def 3;
hence contradiction by A11, A14, A16, FUNCT_1:def 12; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum