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 object ; :: 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 2;
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, Th48; :: 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 Th49;
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 object ; :: 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 Th49;
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 Th48;
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 2;
then x in (F . z) /\ X9 by A11, A10, Th48;
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;