let x be set ; :: according to CARD_FIN:def 3 :: thesis: (Intersect F,G) . x is finite

per cases ( x in dom (Intersect F,G) or not x in dom (Intersect F,G) ) ;

suppose 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) & F . x is finite ) by YELLOW20:def 2;
hence (Intersect F,G) . x is finite ; :: thesis: verum

end;

suppose not x in dom (Intersect F,G) ; :: thesis: (Intersect F,G) . x is finite

hence (Intersect F,G) . x is finite by FUNCT_1:def 4; :: thesis: verum

end;

end;