let a be Nat; :: thesis: for n being non zero Nat holds pfexp (n |^ a) = a * (pfexp n)
let n be non zero Nat; :: thesis: pfexp (n |^ a) = a * (pfexp n)
for i being object st i in SetPrimes holds
(pfexp (n |^ a)) . i = (a * (pfexp n)) . i

proof

let i be object ; :: thesis: ( i in SetPrimes implies (pfexp (n |^ a)) . i = (a * (pfexp n)) . i )
assume i in SetPrimes ; :: thesis: (pfexp (n |^ a)) . i = (a * (pfexp n)) . i
then reconsider x = i as prime Element of NAT by NEWTON:def 6;
thus (pfexp (n |^ a)) . i = x |-count (n |^ a) by Def8
.= a * (x |-count n) by Th32
.= a * ((pfexp n) . i) by Def8
.= (a * (pfexp n)) . i by Def2 ; :: thesis: verum

end;

hence pfexp (n |^ a) = a * (pfexp n) ; :: thesis: verum