let n, p be Nat; :: thesis: ( p is prime implies NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n } )
assume A1: p is prime ; :: thesis: NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n }
for x being object holds
( x in NatDivisors (p |^ n) iff x in { (p |^ k) where k is Element of NAT : k <= n } )

proof

let x be object ; :: thesis: ( x in NatDivisors (p |^ n) iff x in { (p |^ k) where k is Element of NAT : k <= n } )

hereby :: thesis: ( x in { (p |^ k) where k is Element of NAT : k <= n } implies x in NatDivisors (p |^ n) )

assume A2: x in NatDivisors (p |^ n) ; :: thesis: x in { (p |^ k) where k is Element of NAT : k <= n }
then reconsider x9 = x as Nat ;
x9 divides p |^ n by A2, MOEBIUS1:39;
then ex t being Element of NAT st
( x9 = p |^ t & t <= n ) by A1, PEPIN:34;
hence x in { (p |^ k) where k is Element of NAT : k <= n } ; :: thesis: verum

end;

assume x in { (p |^ k) where k is Element of NAT : k <= n } ; :: thesis: x in NatDivisors (p |^ n)
then A3: ex t being Element of NAT st
( x = p |^ t & t <= n ) ;
then reconsider x9 = x as Nat ;
x9 divides p |^ n by A3, NEWTON:89;
hence x in NatDivisors (p |^ n) by A1, A3; :: thesis: verum

end;

hence NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n } by TARSKI:2; :: thesis: verum