let y be set ; :: thesis: for F, Ch being Function st not union (rng F) is empty & Intersection (F,Ch,y) = union (rng F) holds
F | (Ch " {y}) = (Ch " {y}) --> (union (rng F))
let F, Ch be Function; :: thesis: ( not union (rng F) is empty & Intersection (F,Ch,y) = union (rng F) implies F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) )
set ChF = (Ch " {y}) --> (union (rng F));
assume that
A1: not union (rng F) is empty and
A2: Intersection (F,Ch,y) = union (rng F) ; :: thesis: F | (Ch " {y}) = (Ch " {y}) --> (union (rng F))
A3: (dom F) /\ (Ch " {y}) = dom (F | (Ch " {y})) by RELAT_1:61;
(dom F) /\ (Ch " {y}) = Ch " {y} by A1, A2, Th19, XBOOLE_1:28;
then A4: dom (F | (Ch " {y})) = dom ((Ch " {y}) --> (union (rng F))) by A3;
assume F | (Ch " {y}) <> (Ch " {y}) --> (union (rng F)) ; :: thesis: contradiction
then consider x being object such that
A5: x in dom (F | (Ch " {y})) and
A6: (F | (Ch " {y})) . x <> ((Ch " {y}) --> (union (rng F))) . x by A4;
x in (dom F) /\ (Ch " {y}) by A5, RELAT_1:61;
then A7: x in dom F by XBOOLE_0:def 4;
x in (dom F) /\ (Ch " {y}) by A5, RELAT_1:61;
then A8: x in Ch " {y} by XBOOLE_0:def 4;
then A9: ((Ch " {y}) --> (union (rng F))) . x = union (rng F) by FUNCOP_1:7;
Ch . x in {y} by A8, FUNCT_1:def 7;
then A10: Ch . x = y by TARSKI:def 1;
F . x = (F | (Ch " {y})) . x by A5, FUNCT_1:47;
then (F | (Ch " {y})) . x in rng F by A7, FUNCT_1:def 3;
then (F | (Ch " {y})) . x c= ((Ch " {y}) --> (union (rng F))) . x by A9, ZFMISC_1:74;
then not union (rng F) c= (F | (Ch " {y})) . x by A6, A9;
then consider z being object such that
A11: z in union (rng F) and
A12: not z in (F | (Ch " {y})) . x ;
x in dom Ch by A8, FUNCT_1:def 7;
then z in F . x by A2, A11, A10, Def2;
hence contradiction by A5, A12, FUNCT_1:47; :: thesis: verum