F | X is finite ;
hence F | X is finite PartFunc of , ; :: thesis: verum