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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Intersection F,Ch,y) /\ X' or x in Intersection (Intersect F,((dom F) --> X')),Ch,y )
assume A1: x in (Intersection F,Ch,y) /\ X' ; :: thesis: x in Intersection (Intersect F,((dom F) --> X')),Ch,y
A2: for z being set st z in dom Ch & Ch . z = y holds
x in (Intersect F,((dom F) --> X')) . z

proof

A3: x in Intersection F,Ch,y by A1, XBOOLE_0:def 4;
let z be set ; :: thesis: ( z in dom Ch & Ch . z = y implies x in (Intersect F,((dom F) --> X')) . z )
assume ( z in dom Ch & Ch . z = y ) ; :: thesis: x in (Intersect F,((dom F) --> X')) . z
then A4: x in F . z by A3, Def2;
then A5: z in dom F by FUNCT_1:def 4;
x in X' by A1, XBOOLE_0:def 4;
then x in (F . z) /\ X' by A4, XBOOLE_0:def 4;
hence x in (Intersect F,((dom F) --> X')) . z by A5, Th57; :: thesis: verum

end;

x in X' by A1, XBOOLE_0:def 4;
then x in (union (rng F)) /\ X' by A1, XBOOLE_0:def 4;
then x in union (rng (Intersect F,((dom F) --> X'))) by Th58;
hence x in Intersection (Intersect F,((dom F) --> X')),Ch,y by A2, Def2; :: thesis: verum

end;

thus Intersection (Intersect F,((dom F) --> X')),Ch,y c= (Intersection F,Ch,y) /\ X' :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection (Intersect F,((dom F) --> X')),Ch,y or x in (Intersection F,Ch,y) /\ X' )
assume A6: x in Intersection (Intersect F,((dom F) --> X')),Ch,y ; :: thesis: x in (Intersection F,Ch,y) /\ X'
x in union (rng (Intersect F,((dom F) --> X'))) by A6;
then A7: x in (union (rng F)) /\ X' by Th58;
then A8: x in X' by XBOOLE_0:def 4;
A9: for z being set st z in dom Ch & Ch . z = y holds
x in F . z

proof

A10: dom (Intersect F,((dom F) --> X')) = dom F by Th57;
let z be set ; :: thesis: ( z in dom Ch & Ch . z = y implies x in F . z )
assume ( z in dom Ch & Ch . z = y ) ; :: thesis: x in F . z
then A11: x in (Intersect F,((dom F) --> X')) . z by A6, Def2;
then z in dom (Intersect F,((dom F) --> X')) by FUNCT_1:def 4;
then x in (F . z) /\ X' by A11, A10, Th57;
hence x in F . z by XBOOLE_0:def 4; :: thesis: verum

end;

x in union (rng F) by A7, XBOOLE_0:def 4;
then x in Intersection F,Ch,y by A9, Def2;
hence x in (Intersection F,Ch,y) /\ X' by A8, XBOOLE_0:def 4; :: thesis: verum

end;