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