let n be Nat; :: thesis:
let p be Prime; :: thesis:
let m be non zero Nat; :: thesis:
assume A1: p |^ n divides m ; :: thesis:
set n1 = n + 1;
deffunc H₁( Nat) -> set = p |^ $1;
consider f being Function such that
A2: dom f = Segm (n + 1) and
A3: for d being Element of Segm (n + 1) holds f . d = H₁(d) from FUNCT_1:sch 4();
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis:
assume A4: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis:
reconsider x1 = x1, x2 = x2 as Nat by A4, A2;
A5: ( H₁(x1) = f . x1 & H₁(x2) = f . x2 ) by A4, A2, A3;
A6: ( x1 < x2 & p > 1 implies p to_power x1 < p to_power x2 ) by POWER:39;
( x2 < x1 & p > 1 implies p to_power x2 < p to_power x1 ) by POWER:39;
hence x1 = x2 by A6, A5, A4, INT_2:def 4, XXREAL_0:1; :: thesis:

end;

then A7: card (Segm (n + 1)) c= card (rng f) by FUNCT_1:def 4, A2, CARD_1:10;
rng f c= { (p |^ k) where k is Element of NAT : k <= n }

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A8: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A8, A2;
x < n + 1 by A8, A2, NAT_1:44;
then A9: x <= n by NAT_1:13;
f . x = H₁(x) by A2, A3, A8;
hence y in { (p |^ k) where k is Element of NAT : k <= n } by A9, A8; :: thesis:

end;