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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Intersection F,Ch,y) /\ X9 or x in Intersection (Intersect F,((dom F) --> X9)),Ch,y )
assume A1: x in (Intersection F,Ch,y) /\ X9 ; :: thesis: x in Intersection (Intersect F,((dom F) --> X9)),Ch,y
A2: for z being set st z in dom Ch & Ch . z = y holds
x in (Intersect F,((dom F) --> X9)) . 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) --> X9)) . z )
assume ( z in dom Ch & Ch . z = y ) ; :: thesis: x in (Intersect F,((dom F) --> X9)) . z
then A4: x in F . z by A3, Def2;
then A5: z in dom F by FUNCT_1:def 4;
x in X9 by A1, XBOOLE_0:def 4;
then x in (F . z) /\ X9 by A4, XBOOLE_0:def 4;
hence x in (Intersect F,((dom F) --> X9)) . z by A5, Th57; :: thesis: verum

end;

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection (Intersect F,((dom F) --> X9)),Ch,y or x in (Intersection F,Ch,y) /\ X9 )
assume A6: x in Intersection (Intersect F,((dom F) --> X9)),Ch,y ; :: thesis: x in (Intersection F,Ch,y) /\ X9
x in union (rng (Intersect F,((dom F) --> X9))) by A6;
then A7: x in (union (rng F)) /\ X9 by Th58;
then A8: x in X9 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) --> X9)) = 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) --> X9)) . z by A6, Def2;
then z in dom (Intersect F,((dom F) --> X9)) by FUNCT_1:def 4;
then x in (F . z) /\ X9 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) /\ X9 by A8, XBOOLE_0:def 4; :: thesis: verum

end;