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

end;

end;