b > 1 by Def0;
then b |^ (b |-count a) divides a by Def6;
then consider c being Integer such that
A1: a = (b |^ (b |-count a)) * c ;
thus a / (b |^ (b |-count a)) is integer by A1, XCMPLX_1:89; :: thesis: verum