let a, b be Nat; :: thesis: ( not b is empty & a is Prime & a divides b implies a in support (pfexp b) )
assume that
A1: not b is empty and
A2: a is Prime and
A3: a divides b ; :: thesis: a in support (pfexp b)
1 < a by A2, INT_2:def 4;
then A4: a |-count b <> 0 by A1, A3, Th27;
(pfexp b) . a = a |-count b by A2, Def8;
hence a in support (pfexp b) by A4, PRE_POLY:def 7; :: thesis: verum