let n be Element of NAT ; :: thesis:
let p be Prime; :: thesis:
assume A1: n <> 0 ; :: thesis:
defpred S₁[ Nat, set ] means ( ( $2 = 1 implies p |^ $1 divides n ) & ( p |^ $1 divides n implies $2 = 1 ) & ( $2 = 0 implies not p |^ $1 divides n ) & ( not p |^ $1 divides n implies $2 = 0 ) );
A3: for k being Nat st k in Seg n holds
ex x being set st S₁[k,x]

let k be Nat; :: thesis:
assume k in Seg n ; :: thesis:

per cases ;

suppose A4: p |^ k divides n ; :: thesis:

set x = 1;
take 1 ; :: thesis:
thus S₁[k,1] by A4; :: thesis:

end;

suppose A5: not p |^ k divides n ; :: thesis:

set x = 0 ;
take 0 ; :: thesis:
thus S₁[k, 0 ] by A5; :: thesis:

end;

consider f being FinSequence such that
A6: dom f = Seg n and
A7: for k being Nat st k in Seg n holds
S₁[k,f . k] from FINSEQ_1:sch 1(A3);

let x be set ; :: thesis:
assume x in rng f ; :: thesis:
then consider k being set such that
A8: ( k in dom f & f . k = x ) by FUNCT_1:def 5;
reconsider k = k as Element of NAT by A8;
S₁[k,f . k] by A6, A7, A8;
hence x in NAT by A8; :: thesis:

end;

then rng f c= NAT by TARSKI:def 3;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
take f ; :: thesis:
thus len f = n by A6, FINSEQ_1:def 3; :: thesis:
thus for k being Element of NAT st k in dom f holds
( ( f . k = 1 implies p |^ k divides n ) & ( p |^ k divides n implies f . k = 1 ) & ( f . k = 0 implies not p |^ k divides n ) & ( not p |^ k divides n implies f . k = 0 ) ) by A6, A7; :: thesis:
set f1 = ((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0 );
set n1 = p |-count n;
set n2 = n -' (p |-count n);

A9: now

end;

proof

per cases by A18, FINSEQ_1:38;

suppose A19: x1 in dom ((p |-count n) |-> 1) ; :: thesis:

per cases ;

suppose x1 = 0 ; :: thesis:

then p |^ x1 = 1 by NEWTON:9;
hence p |^ x1 divides n by NAT_D:6; :: thesis:

end;

suppose x1 > 0 ; :: thesis:

then x1 + 1 > 0 + 1 by XREAL_1:8;
then x1 >= 1 by NAT_1:13;
then A22: x1 -' 1 = x1 - 1 by XREAL_1:235;
set i = x1 -' 1;
set j = p |-count n;
A23: (x1 -' 1) + 1 = x1 by A22;
A24: (- 1) + x1 < 0 + x1 by XREAL_1:8;
x1 <= p |-count n by A20, FINSEQ_1:3;
then A25: x1 -' 1 < p |-count n by A22, A24, XXREAL_0:2;
p <> 1 by INT_2:def 5;
then p |^ (p |-count n) divides n by A1, NAT_3:def 7;
hence p |^ x1 divides n by A23, A25, NAT_3:4; :: thesis:

end;

hence f . x = (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0 )) . x by A6, A7, A17, A21; :: thesis:

end;

suppose ex m being Nat st
( m in dom ((n -' (p |-count n)) |-> 0 ) & x1 = (len ((p |-count n) |-> 1)) + m ) ; :: thesis:

assume p |^ x1 divides n ; :: thesis:
then A30: p |-count (p |^ x1) <= p |-count n by A1, NAT_3:30;
p > 1 by INT_2:def 5;
hence contradiction by A29, A30, NAT_3:25; :: thesis:

end;

hence f . x = (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0 )) . x by A6, A7, A17, A28; :: thesis:

end;