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:13;
A5: not for y being object holds
( y in (f +* (A --> x)) .: B iff y in f .: B ) by A2, TARSKI:2;

now :: thesis: ( ( 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 ) ; :: 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 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; :: 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 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; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum