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