let p, n be natural number ; :: 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 set holds
( x in NatDivisors (p |^ n) iff x in { (p |^ k) where k is Element of NAT : k <= n } )

proof

let x be set ; :: 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 x' = x as natural number ;
( 0 < x' & x' divides p |^ n ) by A2, MOEBIUS1:39;
then consider t being Element of NAT such that
A3: ( x' = p |^ t & t <= n ) by A1, PEPIN:35;
thus x in { (p |^ k) where k is Element of NAT : k <= n } by A3; :: thesis: verum

end;

assume x in { (p |^ k) where k is Element of NAT : k <= n } ; :: thesis: x in NatDivisors (p |^ n)
then consider t being Element of NAT such that
A4: ( x = p |^ t & t <= n ) ;
reconsider x' = x as natural number by A4;
( 0 < x' & x' divides p |^ n ) by A1, A4, RADIX_1:7;
hence x in NatDivisors (p |^ n) by MOEBIUS1:39; :: thesis: verum

end;

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