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

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

reconsider n = n as non zero Element of NAT by ORDINAL1:def 12;
take n ; :: thesis:
take e = 0 ; :: thesis:
(k + 1) |^ e = 1 by NEWTON:4;
hence ( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) ) by A2; :: thesis:

end;

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

reconsider r = k + 1 as non zero Element of NAT ;
set e = r |-count n;
set s = r |^ (r |-count n);

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

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

end;

hence contradiction by A3; :: thesis:

end;

then k + 1 in support (pfexp n) by NAT_3:def 9;
then A7: r is Prime by NAT_3:34;
then A8: r > 1 by INT_2:def 4;
then r |^ (r |-count n) divides n by NAT_3:def 7;
then consider t being Nat such that
A9: 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 A9, ORDINAL1:def 12;
A10: support (ppf t) = support (pfexp t) by NAT_3:def 9;
A11: support (ppf t) c= Seg k

set f = r |-count t;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A12: x in support (ppf t) ; :: thesis:
then reconsider m = x as Nat ;
A13: x in support (pfexp t) by A12, NAT_3:def 9;

A14: now :: thesis:

assume A15: m = r ; :: thesis:
(pfexp t) . r = r |-count t by A7, NAT_3:def 8;
then r |-count t <> 0 by A13, A15, PRE_POLY:def 7;
then r |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A16: r |-count t = 1 + g by NAT_1:10;
r |^ (r |-count t) divides t by A8, NAT_3:def 7;
then consider u being Nat such that
A17: t = (r |^ (r |-count t)) * u by NAT_D:def 3;
reconsider g = g as Element of NAT by ORDINAL1:def 12;
n = s * (((r |^ g) * r) * u) by A9, A16, A17, NEWTON:6
.= (s * r) * ((r |^ g) * u)
.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:6 ;
then r |^ ((r |-count n) + 1) divides n by NAT_D:def 3;
hence contradiction by A8, NAT_3:def 7; :: thesis:

end;

support (pfexp t) c= support (pfexp n) by A9, NAT_3:45;
then support (ppf t) c= support (ppf n) by A10, NAT_3:def 9;
then m in support (ppf n) by A12;
then m <= k + 1 by A1, FINSEQ_1:1;
then m < r by A14, XXREAL_0:1;
then A18: m <= k by NAT_1:13;
x is Prime by A13, NAT_3:34;
then 1 <= m by INT_2:def 4;
hence x in Seg k by A18, FINSEQ_1:1; :: thesis:

end;

A19: r |-count n <> 0

assume r |-count n = 0 ; :: thesis:
then n = 1 * t by A9, NEWTON:4;
hence contradiction by A3, A11; :: thesis:

end;

take m = t; :: thesis:
take e = (k + 1) |-count n; :: thesis:
support (ppf s) = support (pfexp s) by NAT_3:def 9;
then A20: support (ppf s) = {r} by A7, A19, NAT_3:42;

A21: now :: thesis:

assume support (ppf s) meets support (ppf t) ; :: thesis:
then consider x being object such that
A22: x in support (ppf s) and
A23: x in support (ppf t) by XBOOLE_0:3;
x = r by A20, A22, TARSKI:def 1;
then r <= k by A11, A23, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis:

end;

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 ) )

let p be Prime; :: thesis:

hereby :: thesis:

assume p in support (ppf m) ; :: thesis:
then not p in support (ppf s) by A21, XBOOLE_0:3;
then A24: p |-count s = 0 by Th15;
p |-count n = (p |-count (r |^ e)) + (p |-count t) by A9, NAT_3:28;
hence p |-count m = p |-count n by A24; :: thesis:

end;

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

end;

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 A9, A11; :: thesis:

end;

end;