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