dom F is finite ;
then dom (max+ F) is finite by Def10;
hence max+ F is finite by FINSET_1:10; :: thesis: verum