let x be object ; :: according to FINSET_1:def 4 :: thesis: ( not x in dom (F | X) or (F | X) . x is finite )
assume 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