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
( x in union (rng F) & x in X' ) by A1, XBOOLE_0:def 4;
then x in (union (rng F)) /\ X' by XBOOLE_0:def 4;
then A2: x in union (rng (Intersect F,((dom F) --> X'))) by Th58;
for z being set st z in dom Ch & Ch . z = y holds
x in (Intersect F,((dom F) --> X')) . z

proof

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

end;

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 A4: 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 A4;
then x in (union (rng F)) /\ X' by Th58;
then A5: ( x in union (rng F) & x in X' ) by XBOOLE_0:def 4;
for z being set st z in dom Ch & Ch . z = y holds
x in F . z

proof

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

end;

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

end;