let a, b be Nat; :: thesis: ( 1 < b implies b |-count (b |^ a) = a )
reconsider a = a as Element of NAT by ORDINAL1:def 12;
assume A1: b > 1 ; :: thesis: b |-count (b |^ a) = a
then reconsider b = b as non zero Element of NAT by ORDINAL1:def 12;

now :: thesis: not b |^ (a + 1) divides b |^ a

b |^ a divides b |^ (a + 1) by NAT_1:11, NEWTON:89;
then A2: b |^ a <= b |^ (a + 1) by NAT_D:7;
assume b |^ (a + 1) divides b |^ a ; :: thesis: contradiction
then b |^ (a + 1) <= b |^ a by NAT_D:7;
then b |^ a = b |^ (a + 1) by A2, XXREAL_0:1;
then a + 0 = a + 1 by A1, PEPIN:30;
hence contradiction ; :: thesis: verum

end;

hence b |-count (b |^ a) = a by A1, Def7; :: thesis: verum