let n be Element of NAT ; :: thesis:
let p be Prime; :: thesis:
defpred S₁[ Element of NAT ] means for p being Prime ex f being FinSequence of NAT st
( len f = $1 & ( for k being Element of NAT st k in dom f holds
f . k = [\($1 / (p |^ k))/] ) & p |-count ($1 ! ) = Sum f );
A1: S₁[ 0 ]

proof

let p be Prime; :: thesis:
set f = <*> NAT ;
take <*> NAT ; :: thesis:
thus len (<*> NAT ) = 0 ; :: thesis:
thus for k being Element of NAT st k in dom (<*> NAT ) holds
(<*> NAT ) . k = [\(0 / (p |^ k))/] ; :: thesis:
p <> 1 by INT_2:def 5;
hence p |-count (0 ! ) = Sum (<*> NAT ) by NAT_3:21, NEWTON:18, RVSUM_1:102; :: thesis:

end;

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A3: S₁[n] ; :: thesis:
for p being Prime ex f being FinSequence of NAT st
( len f = n + 1 & ( for k being Element of NAT st k in dom f holds
f . k = [\((n + 1) / (p |^ k))/] ) & p |-count ((n + 1) ! ) = Sum f )

proof

let p be Prime; :: thesis:
consider fn being FinSequence of NAT such that
A4: ( len fn = n & ( for k being Element of NAT st k in dom fn holds
fn . k = [\(n / (p |^ k))/] ) & p |-count (n ! ) = Sum fn ) by A3;
consider fn1 being FinSequence of NAT such that
A5: ( len fn1 = n + 1 & ( for k being Element of NAT st k in dom fn1 holds
( ( fn1 . k = 1 implies p |^ k divides n + 1 ) & ( p |^ k divides n + 1 implies fn1 . k = 1 ) & ( fn1 . k = 0 implies not p |^ k divides n + 1 ) & ( not p |^ k divides n + 1 implies fn1 . k = 0 ) ) ) & p |-count (n + 1) = Sum fn1 ) by Th47;
set f = (fn ^ <*0 *>) + fn1;

now

let y be set ; :: thesis:
assume y in rng ((fn ^ <*0 *>) + fn1) ; :: thesis:
then consider x being set such that
A6: ( x in dom ((fn ^ <*0 *>) + fn1) & y = ((fn ^ <*0 *>) + fn1) . x ) by FUNCT_1:def 5;
thus y in NAT by A6; :: thesis:

end;

then rng ((fn ^ <*0 *>) + fn1) c= NAT by TARSKI:def 3;
then reconsider f = (fn ^ <*0 *>) + fn1 as FinSequence of NAT by FINSEQ_1:def 4;
take f ; :: thesis:
set fn0 = fn ^ <*0 *>;
A7: dom f = (dom (fn ^ <*0 *>)) /\ (dom fn1) by Th41;
A8: len (fn ^ <*0 *>) = (len fn) + (len <*0 *>) by FINSEQ_1:35
.= n + 1 by A4, FINSEQ_1:56 ;
then A9: Seg (n + 1) = dom (fn ^ <*0 *>) by FINSEQ_1:def 3;
Seg (n + 1) = dom fn1 by A5, FINSEQ_1:def 3;
hence len f = n + 1 by A7, A9, FINSEQ_1:def 3; :: thesis:
thus for k being Element of NAT st k in dom f holds
f . k = [\((n + 1) / (p |^ k))/] :: thesis:

proof

let k be Element of NAT ; :: thesis:
assume A10: k in dom f ; :: thesis:
then A11: f . k = ((fn ^ <*0 *>) . k) + (fn1 . k) by VALUED_1:def 1;
A12: ( k in dom (fn ^ <*0 *>) & k in dom fn1 ) by A7, A10, XBOOLE_0:def 4;
A13: (fn ^ <*0 *>) . k = [\(n / (p |^ k))/]

proof

per cases by A12, FINSEQ_1:38;

suppose A14: k in dom fn ; :: thesis:

then fn . k = [\(n / (p |^ k))/] by A4;
hence (fn ^ <*0 *>) . k = [\(n / (p |^ k))/] by A14, FINSEQ_1:def 7; :: thesis:

end;

suppose ex n1 being Nat st
( n1 in dom <*0 *> & k = (len fn) + n1 ) ; :: thesis:

then consider n1 being Nat such that
A15: ( n1 in dom <*0 *> & k = (len fn) + n1 ) ;
n1 in Seg 1 by A15, FINSEQ_1:55;
then A16: n1 = 1 by FINSEQ_1:4, TARSKI:def 1;
then (fn ^ <*0 *>) . (n + 1) = <*0 *> . 1 by A4, A15, FINSEQ_1:def 7;
then A17: (fn ^ <*0 *>) . k = 0 by A4, A15, A16, FINSEQ_1:57;
A18: p |^ (n + 1) = (p |^ n) * p by NEWTON:11;
A19: p > 1 by INT_2:def 5;
then A20: p * (p |^ n) > 1 * (p |^ n) by XREAL_1:70;
p |^ n > n by A19, Th3;
then p |^ k > n by A4, A15, A16, A18, A20, XXREAL_0:2;
then n / (p |^ k) < 1 by XREAL_1:191;
then (n / (p |^ k)) - 1 < 1 - 1 by XREAL_1:11;
hence (fn ^ <*0 *>) . k = [\(n / (p |^ k))/] by A17, INT_1:def 4; :: thesis:

end;

p > 1 by INT_2:def 5;
then A21: p |^ k >= 1 by PREPOWER:19;
A22: (p |^ k) / (p |^ k) = 1 by XCMPLX_1:60;

per cases ;

suppose A23: p |^ k divides n + 1 ; :: thesis:

then consider r being Nat such that
A24: n + 1 = (p |^ k) * r by NAT_D:def 3;
A25: (n + 1) / (p |^ k) = r / ((p |^ k) / (p |^ k)) by A24, XCMPLX_1:78
.= r / (1 / 1) by XCMPLX_1:60
.= r ;
B26: (p |^ k) - 1 >= 1 - 1 by A21, XREAL_1:11;
(((p |^ k) / (p |^ k)) + ((- 1) / (p |^ k))) - 1 < 0 by A22;
then A27: (((p |^ k) + (- 1)) / (p |^ k)) - 1 < 0 by XCMPLX_1:63;
[\(n / (p |^ k))/] + 1 = [\((n / (p |^ k)) + 1)/] by INT_1:51
.= [\((n / (p |^ k)) + ((p |^ k) / (p |^ k)))/] by XCMPLX_1:60
.= [\((n + (p |^ k)) / (p |^ k))/] by XCMPLX_1:63
.= [\(((n + 1) + ((p |^ k) - 1)) / (p |^ k))/]
.= [\(((n + 1) / (p |^ k)) + (((p |^ k) - 1) / (p |^ k)))/] by XCMPLX_1:63
.= ((n + 1) / (p |^ k)) + [\(((p |^ k) - 1) / (p |^ k))/] by A25, INT_1:51
.= ((n + 1) / (p |^ k)) + 0 by B26, A27, INT_1:def 4
.= [\((n + 1) / (p |^ k))/] by A25, INT_1:47 ;
hence f . k = [\((n + 1) / (p |^ k))/] by A5, A11, A12, A13, A23; :: thesis:

end;

suppose A28: not p |^ k divides n + 1 ; :: thesis:

end;

reconsider fn0 = fn ^ <*0 *> as Element of (n + 1) -tuples_on REAL by A8, FINSEQ_2:110;
reconsider fn1 = fn1 as Element of (n + 1) -tuples_on REAL by A5, FINSEQ_2:110;
A35: Sum f = (Sum fn0) + (Sum fn1) by RVSUM_1:119
.= ((Sum fn) + 0 ) + (p |-count (n + 1)) by A5, RVSUM_1:104
.= (p |-count (n ! )) + (p |-count (n + 1)) by A4 ;
( n ! <> 0 & n + 1 <> 0 ) by NEWTON:23;
then (p |-count (n ! )) + (p |-count (n + 1)) = p |-count ((n ! ) * (n + 1)) by NAT_3:28
.= p |-count ((n + 1) ! ) by NEWTON:21 ;
hence p |-count ((n + 1) ! ) = Sum f by A35; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
then consider f being FinSequence of NAT such that
A36: ( len f = n & ( for k being Element of NAT st k in dom f holds
f . k = [\(n / (p |^ k))/] ) & p |-count (n ! ) = Sum f ) ;
take f ; :: thesis:
thus ( len f = n & ( for k being Element of NAT st k in dom f holds
f . k = [\(n / (p |^ k))/] ) & p |-count (n ! ) = Sum f ) by A36; :: thesis: