let a, b be Nat; :: thesis: ( b <> 1 & a <> 0 & b divides b |^ (b |-count a) implies b divides a )
assume that
A1: ( b <> 1 & a <> 0 ) and
A2: b divides b |^ (b |-count a) ; :: thesis: b divides a
b |^ (b |-count a) divides a by A1, Def7;
hence b divides a by A2, NAT_D:4; :: thesis: verum