let X' be set ; :: thesis: for F being Function holds
( dom (Intersect F,((dom F) --> X')) = dom F & ( for x being set st x in dom F holds
(Intersect F,((dom F) --> X')) . x = (F . x) /\ X' ) )
let F be Function; :: thesis: ( dom (Intersect F,((dom F) --> X')) = dom F & ( for x being set st x in dom F holds
(Intersect F,((dom F) --> X')) . x = (F . x) /\ X' ) )
dom ((dom F) --> X') = dom F by FUNCOP_1:19;
then A1: (dom F) /\ (dom ((dom F) --> X')) = dom F ;
hence dom F = dom (Intersect F,((dom F) --> X')) by YELLOW20:def 2; :: thesis: for x being set st x in dom F holds
(Intersect F,((dom F) --> X')) . x = (F . x) /\ X'
let x be set ; :: thesis: ( x in dom F implies (Intersect F,((dom F) --> X')) . x = (F . x) /\ X' )
assume A2: x in dom F ; :: thesis: (Intersect F,((dom F) --> X')) . x = (F . x) /\ X'
then (Intersect F,((dom F) --> X')) . x = (F . x) /\ (((dom F) --> X') . x) by A1, YELLOW20:def 2;
hence (Intersect F,((dom F) --> X')) . x = (F . x) /\ X' by A2, FUNCOP_1:13; :: thesis: verum