let n, m be non zero Nat; :: thesis: ( m divides n implies pfexp (n div m) = (pfexp n) -' (pfexp m) )
assume A1: m divides n ; :: thesis: pfexp (n div m) = (pfexp n) -' (pfexp m)
for i being object st i in SetPrimes holds
(pfexp (n div m)) . i = ((pfexp n) -' (pfexp m)) . i

proof

let i be object ; :: thesis: ( i in SetPrimes implies (pfexp (n div m)) . i = ((pfexp n) -' (pfexp m)) . i )
assume i in SetPrimes ; :: thesis: (pfexp (n div m)) . i = ((pfexp n) -' (pfexp m)) . i
then reconsider a = i as prime Element of NAT by NEWTON:def 6;
thus (pfexp (n div m)) . i = a |-count (n div m) by Def8
.= (a |-count n) -' (a |-count m) by A1, Th31
.= ((pfexp n) . i) -' (a |-count m) by Def8
.= ((pfexp n) . i) -' ((pfexp m) . i) by Def8
.= ((pfexp n) -' (pfexp m)) . i by PRE_POLY:def 6 ; :: thesis: verum

end;

hence pfexp (n div m) = (pfexp n) -' (pfexp m) ; :: thesis: verum