let X9 be set ; :: thesis: for F being Function holds (union (rng F)) /\ X9 = union (rng (Intersect (F,((dom F) --> X9))))
let F be Function; :: thesis: (union (rng F)) /\ X9 = union (rng (Intersect (F,((dom F) --> X9))))
set I = Intersect (F,((dom F) --> X9));
thus (union (rng F)) /\ X9 c= union (rng (Intersect (F,((dom F) --> X9)))) :: according to XBOOLE_0:def 10 :: thesis: union (rng (Intersect (F,((dom F) --> X9)))) c= (union (rng F)) /\ X9

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union (rng F)) /\ X9 or x in union (rng (Intersect (F,((dom F) --> X9)))) )
assume A1: x in (union (rng F)) /\ X9 ; :: thesis: x in union (rng (Intersect (F,((dom F) --> X9))))
A2: x in X9 by A1, XBOOLE_0:def 4;
x in union (rng F) by A1, XBOOLE_0:def 4;
then consider Fx being set such that
A3: x in Fx and
A4: Fx in rng F by TARSKI:def 4;
consider x1 being object such that
A5: x1 in dom F and
A6: F . x1 = Fx by A4, FUNCT_1:def 3;
x1 in dom (Intersect (F,((dom F) --> X9))) by A5, Th48;
then A7: (Intersect (F,((dom F) --> X9))) . x1 in rng (Intersect (F,((dom F) --> X9))) by FUNCT_1:def 3;
(Intersect (F,((dom F) --> X9))) . x1 = Fx /\ X9 by A5, A6, Th48;
then x in (Intersect (F,((dom F) --> X9))) . x1 by A3, A2, XBOOLE_0:def 4;
hence x in union (rng (Intersect (F,((dom F) --> X9)))) by A7, TARSKI:def 4; :: thesis: verum

end;

thus union (rng (Intersect (F,((dom F) --> X9)))) c= (union (rng F)) /\ X9 :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng (Intersect (F,((dom F) --> X9)))) or x in (union (rng F)) /\ X9 )
assume x in union (rng (Intersect (F,((dom F) --> X9)))) ; :: thesis: x in (union (rng F)) /\ X9
then consider Ix being set such that
A8: x in Ix and
A9: Ix in rng (Intersect (F,((dom F) --> X9))) by TARSKI:def 4;
consider x1 being object such that
A10: x1 in dom (Intersect (F,((dom F) --> X9))) and
A11: (Intersect (F,((dom F) --> X9))) . x1 = Ix by A9, FUNCT_1:def 3;
A12: x1 in dom F by A10, Th48;
then A13: F . x1 in rng F by FUNCT_1:def 3;
A14: (Intersect (F,((dom F) --> X9))) . x1 = (F . x1) /\ X9 by A12, Th48;
then x in F . x1 by A8, A11, XBOOLE_0:def 4;
then A15: x in union (rng F) by A13, TARSKI:def 4;
x in X9 by A8, A11, A14, XBOOLE_0:def 4;
hence x in (union (rng F)) /\ X9 by A15, XBOOLE_0:def 4; :: thesis: verum

end;