dom A = dom (b -leading_coeff A) by Def3;
hence b -leading_coeff A is empty ; :: thesis: verum