let a, b be Nat; ( 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
; 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; verum