let k be Element of NAT ; :: thesis:
let n be non zero Element of NAT ; :: thesis:
assume A1: support (ppf n) c= Seg (k + 1) ; :: thesis:

per cases ;

suppose A2: support (ppf n) c= Seg k ; :: thesis:

take m = n; :: thesis:
take e = 0 ; :: thesis:
(k + 1) |^ e = 1 by NEWTON:9;
hence ( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) ) by A2; :: thesis:

end;

suppose A3: not support (ppf n) c= Seg k ; :: thesis:

A4: now

assume A5: not k + 1 in support (ppf n) ; :: thesis:
support (ppf n) c= Seg k

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A6: x in support (ppf n) ; :: thesis:
then A7: x in support (pfexp n) by NAT_3:def 9;
then A8: x is Prime by NAT_3:34;
reconsider m = x as natural number by A7;
A9: 1 <= m by A8, INT_2:def 5;
m <= k + 1 by A1, A6, FINSEQ_1:3;
then m < k + 1 by A5, A6, XXREAL_0:1;
then m <= k by NAT_1:13;
hence x in Seg k by A9, FINSEQ_1:3; :: thesis:

end;

hence contradiction by A3; :: thesis:

end;

reconsider r = k + 1 as non zero Element of NAT ;
set e = r |-count n;
set s = r |^ (r |-count n);
k + 1 in support (pfexp n) by A4, NAT_3:def 9;
then A10: r is Prime by NAT_3:34;
then A11: r > 1 by INT_2:def 5;
then r |^ (r |-count n) divides n by NAT_3:def 7;
then consider t being Nat such that
A12: n = (r |^ (r |-count n)) * t by NAT_D:def 3;
reconsider s = r |^ (r |-count n), t = t as non zero Element of NAT by A12, ORDINAL1:def 13;
A13: support (ppf t) = support (pfexp t) by NAT_3:def 9;
A14: support (ppf t) c= Seg k

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A15: x in support (ppf t) ; :: thesis:
then A16: x in support (pfexp t) by NAT_3:def 9;
then A17: x is Prime by NAT_3:34;
reconsider m = x as natural number by A16;
A18: 1 <= m by A17, INT_2:def 5;
support (pfexp t) c= support (pfexp n) by A12, NAT_3:45;
then support (ppf t) c= support (ppf n) by A13, NAT_3:def 9;
then m in support (ppf n) by A15;
then A19: m <= k + 1 by A1, FINSEQ_1:3;
set f = r |-count t;

assume A20: m = r ; :: thesis:
(pfexp t) . r = r |-count t by A10, NAT_3:def 8;
then r |-count t <> 0 by A16, A20, POLYNOM1:def 7;
then r |-count t > 0 ;
then r |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A21: r |-count t = 1 + g by NAT_1:10;
reconsider g = g as Element of NAT by ORDINAL1:def 13;
r |^ (r |-count t) divides t by A11, NAT_3:def 7;
then consider u being Nat such that
A22: t = (r |^ (r |-count t)) * u by NAT_D:def 3;
n = s * (((r |^ g) * r) * u) by A12, A21, A22, NEWTON:11
.= (s * r) * ((r |^ g) * u)
.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:11 ;
then r |^ ((r |-count n) + 1) divides n by NAT_D:def 3;
hence contradiction by A11, NAT_3:def 7; :: thesis:

end;

then m < r by A19, XXREAL_0:1;
then m <= k by NAT_1:13;
hence x in Seg k by A18, FINSEQ_1:3; :: thesis:

end;

A23: r |-count n <> 0

assume r |-count n = 0 ; :: thesis:
then n = 1 * t by A12, NEWTON:9;
hence contradiction by A3, A14; :: thesis:

end;

support (ppf s) = support (pfexp s) by NAT_3:def 9;
then A24: support (ppf s) = {r} by A10, A23, NAT_3:42;

A25: now

assume support (ppf s) meets support (ppf t) ; :: thesis:
then consider x being set such that
A26: x in support (ppf s) and
A27: x in support (ppf t) by XBOOLE_0:3;
x = r by A24, A26, TARSKI:def 1;
then r <= k by A14, A27, FINSEQ_1:3;
hence contradiction by NAT_1:13; :: thesis:

end;

proof

let p be Prime; :: thesis:

hereby :: thesis:

end;

assume not p in support (ppf m) ; :: thesis:
hence p |-count m <= p |-count n by Th15; :: thesis:

end;

end;