let n be Element of NAT ; :: thesis: for p being Prime st n <> 0 holds
ex f being FinSequence of NAT st
( len f = n & ( 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 ) ) ) & p |-count n = Sum f )
let p be Prime; :: thesis: ( n <> 0 implies ex f being FinSequence of NAT st
( len f = n & ( 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 ) ) ) & p |-count n = Sum f ) )
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 ) );
set f1 = ((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0);
set n1 = p |-count n;
set n2 = n -' (p |-count n);
set fa = (p |-count n) |-> 1;
set fb = (n -' (p |-count n)) |-> 0;
A1: Sum (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) = (Sum ((p |-count n) |-> 1)) + (Sum ((n -' (p |-count n)) |-> 0)) by RVSUM_1:75
.= ((p |-count n) * 1) + (Sum ((n -' (p |-count n)) |-> 0)) by RVSUM_1:80
.= (p |-count n) + ((n -' (p |-count n)) * 0) by RVSUM_1:80 ;
assume A2: n <> 0 ; :: thesis: ex f being FinSequence of NAT st
( len f = n & ( 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 ) ) ) & p |-count n = Sum f )

A3: now

p <> 1 by INT_2:def 4;
then p |^ (p |-count n) divides n by A2, NAT_3:def 7;
then A4: p |^ (p |-count n) <= n by A2, NAT_D:7;
A5: p > 1 by INT_2:def 4;
assume n < p |-count n ; :: thesis: contradiction
then p to_power n < p to_power (p |-count n) by A5, POWER:39;
then p |^ n < p to_power (p |-count n) by POWER:41;
then p |^ n < p |^ (p |-count n) by POWER:41;
then p |^ n < n by A4, XXREAL_0:2;
hence contradiction by A5, Th3; :: thesis: verum

end;

A6: for k being Nat st k in Seg n holds
ex x being set st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg n implies ex x being set st S₁[k,x] )
assume k in Seg n ; :: thesis: ex x being set st S₁[k,x]

per cases ( p |^ k divides n or not p |^ k divides n ) ;

suppose A7: p |^ k divides n ; :: thesis: ex x being set st S₁[k,x]

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

end;

suppose A8: not p |^ k divides n ; :: thesis: ex x being set st S₁[k,x]

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

end;

end;

end;

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

now

let x be set ; :: thesis: ( x in rng f implies x in NAT )
assume x in rng f ; :: thesis: x in NAT
then consider k being set such that
A11: k in dom f and
A12: f . k = x by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A11;
S₁[k,f . k] by A9, A10, A11;
hence x in NAT by A12; :: thesis: verum

end;

then rng f c= NAT by TARSKI:def 3;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
A13: len (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) = (len ((p |-count n) |-> 1)) + (len ((n -' (p |-count n)) |-> 0)) by FINSEQ_1:22
.= (p |-count n) + (len ((n -' (p |-count n)) |-> 0)) by CARD_1:def 7
.= (p |-count n) + (n -' (p |-count n)) by CARD_1:def 7
.= (p |-count n) + (n - (p |-count n)) by A3, XREAL_1:233 ;
A14: for x being set st x in dom f holds
f . x = (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) . x

proof

set ff2 = (n -' (p |-count n)) |-> 0;
set ff1 = (p |-count n) |-> 1;
let x be set ; :: thesis: ( x in dom f implies f . x = (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) . x )
assume A15: x in dom f ; :: thesis: f . x = (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) . x
then reconsider x1 = x as Element of NAT ;
A16: x in dom (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) by A9, A13, A15, FINSEQ_1:def 3;

per cases ( x1 in dom ((p |-count n) |-> 1) or ex m being Nat st
( m in dom ((n -' (p |-count n)) |-> 0) & x1 = (len ((p |-count n) |-> 1)) + m ) ) by A16, FINSEQ_1:25;

suppose A17: x1 in dom ((p |-count n) |-> 1) ; :: thesis: f . x = (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) . x

then A18: x in Seg (p |-count n) by FUNCOP_1:13;
A19: p |^ x1 divides n

proof

per cases ( x1 = 0 or x1 > 0 ) ;

suppose x1 = 0 ; :: thesis: p |^ x1 divides n

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

end;

suppose x1 > 0 ; :: thesis: p |^ x1 divides n

then x1 + 1 > 0 + 1 by XREAL_1:6;
then x1 >= 1 by NAT_1:13;
then A20: x1 -' 1 = x1 - 1 by XREAL_1:233;
set j = p |-count n;
set i = x1 -' 1;
p <> 1 by INT_2:def 4;
then A21: p |^ (p |-count n) divides n by A2, NAT_3:def 7;
( (- 1) + x1 < 0 + x1 & x1 <= p |-count n ) by A18, FINSEQ_1:1, XREAL_1:6;
then A22: x1 -' 1 < p |-count n by A20, XXREAL_0:2;
(x1 -' 1) + 1 = x1 by A20;
hence p |^ x1 divides n by A22, A21, NAT_3:4; :: thesis: verum

end;

end;

end;

((p |-count n) |-> 1) . x = 1 by A18, FUNCOP_1:7;
then (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) . x1 = 1 by A17, FINSEQ_1:def 7;
hence f . x = (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) . x by A9, A10, A15, A19; :: thesis: verum

end;

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

then consider m being Nat such that
A23: m in dom ((n -' (p |-count n)) |-> 0) and
A24: x = (len ((p |-count n) |-> 1)) + m ;
A25: m in Seg (n -' (p |-count n)) by A23, FUNCOP_1:13;
then m >= 1 by FINSEQ_1:1;
then m + (p |-count n) > 0 + (p |-count n) by XREAL_1:6;
then A26: x1 > p |-count n by A24, CARD_1:def 7;
A27: not p |^ x1 divides n

proof

assume p |^ x1 divides n ; :: thesis: contradiction
then A28: p |-count (p |^ x1) <= p |-count n by A2, NAT_3:30;
p > 1 by INT_2:def 4;
hence contradiction by A26, A28, NAT_3:25; :: thesis: verum

end;

((n -' (p |-count n)) |-> 0) . m = 0 by A25, FUNCOP_1:7;
then (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) . x = 0 by A23, A24, FINSEQ_1:def 7;
hence f . x = (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) . x by A9, A10, A15, A27; :: thesis: verum

end;

end;

end;

take f ; :: thesis: ( len f = n & ( 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 ) ) ) & p |-count n = Sum f )
thus len f = n by A9, FINSEQ_1:def 3; :: thesis: ( ( 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 ) ) ) & p |-count n = Sum f )
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 A9, A10; :: thesis: p |-count n = Sum f
dom f = dom (((p |-count n) |-> 1) ^ ((n -' (p |-count n)) |-> 0)) by A9, A13, FINSEQ_1:def 3;
hence p |-count n = Sum f by A14, A1, FUNCT_1:2; :: thesis: verum