let a, b be Nat; :: thesis: ( a in support (pfexp b) implies a divides b )
set f = pfexp b;
assume A1: a in support (pfexp b) ; :: thesis: a divides b
then reconsider a = a as Prime by Th34;
A2: ( a <> 1 & (pfexp b) . a = a |-count b ) by Def8, INT_2:def 4;
(pfexp b) . a <> 0 by A1, PRE_POLY:def 7;
hence a divides b by A2, Th27; :: thesis: verum