let x be object ; :: according to FINSET_1:def 4 :: thesis: ( not x in dom (Intersect (F,G)) or (Intersect (F,G)) . x is finite )
assume x in dom (Intersect (F,G)) ; :: thesis: (Intersect (F,G)) . x is finite
then x in (dom F) /\ (dom G) by YELLOW20:def 2;
then (Intersect (F,G)) . x = (F . x) /\ (G . x) by YELLOW20:def 2;
hence (Intersect (F,G)) . x is finite ; :: thesis: verum