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 ) )
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:7; :: thesis: verum