A1: now

let F be FinSequence of SetPrimes ; :: thesis:
rng F c= REAL ;
hence F is FinSequence of REAL by FINSEQ_1:def 4; :: thesis:

end;

defpred S₁[ Element of NAT ] means for a, k being Element of NAT
for X being set
for F being FinSequence of SetPrimes
for p being Prime st X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F & len F = $1 holds
( ( p in rng F implies p |-count a = 1 ) & ( not p in rng F implies p |-count a = 0 ) );
A2: S₁[ 0 ]

let a, k be Element of NAT ; :: thesis:
let X be set ; :: thesis:
let F be FinSequence of SetPrimes ; :: thesis:
let p be Prime; :: thesis:
assume A3: ( X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F & len F = 0 ) ; :: thesis:
assume A4: ( ( p in rng F & not p |-count a = 1 ) or ( not p in rng F & not p |-count a = 0 ) ) ; :: thesis:
A5: F = <*> REAL by A3;

per cases by A4;

suppose A6: ( p in rng F & not p |-count a = 1 ) ; :: thesis:

thus contradiction by A5, A6; :: thesis:

end;

suppose A7: ( not p in rng F & not p |-count a = 0 ) ; :: thesis:

( a = 1 & p <> 1 ) by A3, FINSEQ_1:32, INT_2:def 5, RVSUM_1:124;
hence contradiction by A7, NAT_3:21; :: thesis:

end;

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

let n be Element of NAT ; :: thesis:
assume A9: S₁[n] ; :: thesis:
for a, k being Element of NAT
for X being set
for F being FinSequence of SetPrimes
for p being Prime st X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F & len F = n + 1 holds
( ( p in rng F implies p |-count a = 1 ) & ( not p in rng F implies p |-count a = 0 ) )

let a, k be Element of NAT ; :: thesis:
let X be set ; :: thesis:
let F be FinSequence of SetPrimes ; :: thesis:
let p be Prime; :: thesis:
assume A10: ( X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F ) ; :: thesis:
assume A11: len F = n + 1 ; :: thesis:
set x = F . (n + 1);
A12: Seg (n + 1) = dom F by A11, FINSEQ_1:def 3;
then n + 1 in dom F by FINSEQ_1:5;
then A13: F . (n + 1) in rng F by FUNCT_1:def 5;
rng F c= SetPrimes by FINSEQ_1:def 4;
then reconsider x = F . (n + 1) as Prime by A13, NEWTON:def 6;
set X1 = X \ {x};
A14: X \ {x} c= X by XBOOLE_1:36;
then A15: X \ {x} c= SetPrimes by A10, XBOOLE_1:1;
A16: X \ {x} c= Seg k by A10, A14, XBOOLE_1:1;
set F1 = Sgm (X \ {x});
reconsider F1 = Sgm (X \ {x}) as FinSequence of NAT ;
set a1 = Product F1;
set F2 = Sgm {x};
A17: rng F = X by A10, FINSEQ_1:def 13;

let y be set ; :: thesis:
assume y in {x} ; :: thesis:
then y = x by TARSKI:def 1;
hence y in Seg k by A10, A13, A17; :: thesis:

end;

then A18: {x} c= Seg k by TARSKI:def 3;
A19: for m1, n1 being Element of NAT st m1 in X \ {x} & n1 in {x} holds
m1 < n1

let m1, n1 be Element of NAT ; :: thesis:
assume A20: ( m1 in X \ {x} & n1 in {x} ) ; :: thesis:
then A21: m1 in rng F by A14, A17;
A22: F is one-to-one by A10, FINSEQ_3:99;
then A23: m1 in dom (F " ) by A21, FUNCT_1:55;
set l = (F " ) . m1;
(F " ) . m1 in rng (F " ) by A23, FUNCT_1:def 5;
then A24: (F " ) . m1 in Seg (n + 1) by A12, A22, FUNCT_1:55;
then reconsider l = (F " ) . m1 as Element of NAT ;
A25: ( 1 <= l & l <= n + 1 ) by A24, FINSEQ_1:3;
set n' = n + 1;
A26: m1 = F . l by A14, A17, A20, A22, FUNCT_1:57;
A27: n1 = F . (n + 1) by A20, TARSKI:def 1;
not n + 1 = l by A20, A26, ZFMISC_1:64;
then l < n + 1 by A25, XXREAL_0:1;
hence m1 < n1 by A10, A11, A25, A26, A27, FINSEQ_1:def 13; :: thesis:

end;

A28: (X \ {x}) \/ {x} = X \/ {x} by XBOOLE_1:39
.= X by A13, A17, ZFMISC_1:46 ;
then A29: F = F1 ^ (Sgm {x}) by A10, A16, A18, A19, FINSEQ_3:48;
then A30: len F = (len F1) + (len (Sgm {x})) by FINSEQ_1:35;
A31: Sgm {x} = <*x*> by FINSEQ_3:50;
then A32: n + 1 = (len F1) + 1 by A11, A30, FINSEQ_1:56;
A33: rng F c= SetPrimes by FINSEQ_1:def 4;
rng F1 c= rng F by A29, FINSEQ_1:42;
then A34: rng F1 c= SetPrimes by A33, XBOOLE_1:1;
then reconsider F1 = F1 as FinSequence of SetPrimes by FINSEQ_1:def 4;
A35: rng (Sgm {x}) = {x} by A31, FINSEQ_1:56;
A36: Product F = Product (F1 ^ (Sgm {x})) by A10, A16, A18, A19, A28, FINSEQ_3:48
.= Product (F1 ^ <*x*>) by FINSEQ_3:50
.= (Product F1) * x by RVSUM_1:126 ;

let k be Element of NAT ; :: thesis:
assume k in dom F1 ; :: thesis:
then F1 . k in rng F1 by FUNCT_1:def 5;
then F1 . k is Prime by A34, NEWTON:def 6;
hence F1 . k > 0 ; :: thesis:

end;

then Product F1 <> 0 by Th42;
then A37: p |-count a = (p |-count (Product F1)) + (p |-count x) by A10, A36, NAT_3:28;
A38: rng F1 = X \ {x} by A16, FINSEQ_1:def 13;

A39: now

assume p in rng F ; :: thesis:
then p in (rng F1) \/ (rng (Sgm {x})) by A29, FINSEQ_1:44;
then A40: ( p in rng F1 or p in {x} ) by A35, XBOOLE_0:def 3;
A41: p > 1 by INT_2:def 5;

per cases by A40, TARSKI:def 1;

suppose A42: p in rng F1 ; :: thesis:

then not p in {x} by A38, XBOOLE_0:def 5;
then p <> x by TARSKI:def 1;
then p |-count x = 0 by A41, NAT_3:24;
hence p |-count a = 1 by A9, A15, A16, A32, A37, A42; :: thesis:

end;

suppose A43: p = x ; :: thesis:

then p in {x} by TARSKI:def 1;
then not p in rng F1 by A38, XBOOLE_0:def 5;
then p |-count (Product F1) = 0 by A9, A15, A16, A32;
hence p |-count a = 1 by A37, A41, A43, NAT_3:22; :: thesis:

end;

now

assume not p in rng F ; :: thesis:
then not p in (rng F1) \/ (rng (Sgm {x})) by A29, FINSEQ_1:44;
then ( not p in rng F1 & not p in {x} ) by A35, XBOOLE_0:def 3;
then A44: ( p |-count (Product F1) = 0 & p <> x ) by A9, A15, A16, A32, TARSKI:def 1;
p <> 1 by INT_2:def 5;
hence p |-count a = 0 by A37, A44, NAT_3:24; :: thesis:

end;

hence ( ( p in rng F implies p |-count a = 1 ) & ( not p in rng F implies p |-count a = 0 ) ) by A39; :: thesis:

end;

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

end;

A45: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A8);
let a, k be Element of NAT ; :: thesis:
let X be set ; :: thesis:
let F be FinSequence of SetPrimes ; :: thesis:
let p be Prime; :: thesis:
reconsider F = F as FinSequence of REAL by A1;
ex n being Element of NAT st n = len F ;
hence ( X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F implies ( ( p in rng F implies p |-count a = 1 ) & ( not p in rng F implies p |-count a = 0 ) ) ) by A45; :: thesis: