let x be set ; :: according to CARD_FIN:def 3 :: thesis: (F | X) . x is finite

per cases ( x in dom (F | X) or not x in dom (F | X) ) ;

suppose x in dom (F | X) ; :: thesis: (F | X) . x is finite

then (F | X) . x = F . x by FUNCT_1:47;
hence (F | X) . x is finite ; :: thesis: verum

end;

suppose not x in dom (F | X) ; :: thesis: (F | X) . x is finite

hence (F | X) . x is finite by FUNCT_1:def 2; :: thesis: verum

end;

end;