dom A = dom (b -exponent A) by Def1;
hence b -exponent A is empty ; :: thesis: verum