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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (union (rng F)) /\ X' or x in union (rng (Intersect F,((dom F) --> X'))) )
assume A1: x in (union (rng F)) /\ X' ; :: thesis: x in union (rng (Intersect F,((dom F) --> X')))
x in union (rng F) by A1, XBOOLE_0:def 4;
then consider Fx being set such that
A2: ( x in Fx & Fx in rng F ) by TARSKI:def 4;
consider x1 being set such that
A3: ( x1 in dom F & F . x1 = Fx ) by A2, FUNCT_1:def 5;
( x in X' & (Intersect F,((dom F) --> X')) . x1 = Fx /\ X' & x1 in dom (Intersect F,((dom F) --> X')) ) by A1, A3, Th57, XBOOLE_0:def 4;
then ( x in (Intersect F,((dom F) --> X')) . x1 & (Intersect F,((dom F) --> X')) . x1 in rng (Intersect F,((dom F) --> X')) ) by A2, FUNCT_1:def 5, XBOOLE_0:def 4;
hence x in union (rng (Intersect F,((dom F) --> X'))) by TARSKI:def 4; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng (Intersect F,((dom F) --> X'))) or x in (union (rng F)) /\ X' )
assume A4: x in union (rng (Intersect F,((dom F) --> X'))) ; :: thesis: x in (union (rng F)) /\ X'
consider Ix being set such that
A5: ( x in Ix & Ix in rng (Intersect F,((dom F) --> X')) ) by A4, TARSKI:def 4;
consider x1 being set such that
A6: ( x1 in dom (Intersect F,((dom F) --> X')) & (Intersect F,((dom F) --> X')) . x1 = Ix ) by A5, FUNCT_1:def 5;
x1 in dom F by A6, Th57;
then ( x1 in dom F & (Intersect F,((dom F) --> X')) . x1 = (F . x1) /\ X' ) by Th57;
then ( x in F . x1 & F . x1 in rng F & x in X' ) by A5, A6, FUNCT_1:def 5, XBOOLE_0:def 4;
then ( x in union (rng F) & x in X' ) by TARSKI:def 4;
hence x in (union (rng F)) /\ X' by XBOOLE_0:def 4; :: thesis: verum

end;