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