dom A = dom (b -leading_coeff A) by Def3;
hence not b -leading_coeff A is finite by FINSET_1:10; :: thesis: verum