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:
defpred S₁[ natural number ] 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 ) );

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

end;

then reconsider F = F as FinSequence of REAL ;
A1: ex n being Element of NAT st n = len F ;
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

let n be Element of NAT ; :: thesis:
assume A3: 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 that
A4: X c= SetPrimes and
A5: X c= Seg k and
A6: F = Sgm X and
A7: a = Product F ; :: thesis:
set x = F . (n + 1);
assume A8: len F = n + 1 ; :: thesis:
then A9: Seg (n + 1) = dom F by FINSEQ_1:def 3;
then n + 1 in dom F by FINSEQ_1:3;
then A10: F . (n + 1) in rng F by FUNCT_1:def 3;
rng F c= SetPrimes by FINSEQ_1:def 4;
then reconsider x = F . (n + 1) as Prime by A10, NEWTON:def 6;
set X1 = X \ {x};
A11: X \ {x} c= X by XBOOLE_1:36;
then A12: X \ {x} c= Seg k by A5, XBOOLE_1:1;
A13: rng F = X by A5, A6, 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 A5, A10, A13; :: thesis:

end;

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

set n9 = n + 1;
let m1, n1 be Element of NAT ; :: thesis:
assume that
A16: m1 in X \ {x} and
A17: n1 in {x} ; :: thesis:
set l = (F ") . m1;
A18: F is one-to-one by A5, A6, FINSEQ_3:92;
m1 in rng F by A11, A13, A16;
then m1 in dom (F ") by A18, FUNCT_1:33;
then (F ") . m1 in rng (F ") by FUNCT_1:def 3;
then A19: (F ") . m1 in Seg (n + 1) by A9, A18, FUNCT_1:33;
then reconsider l = (F ") . m1 as Element of NAT ;
A20: l <= n + 1 by A19, FINSEQ_1:1;
A21: m1 = F . l by A11, A13, A16, A18, FUNCT_1:35;
then not n + 1 = l by A16, ZFMISC_1:56;
then A22: l < n + 1 by A20, XXREAL_0:1;
A23: n1 = F . (n + 1) by A17, TARSKI:def 1;
1 <= l by A19, FINSEQ_1:1;
hence m1 < n1 by A5, A6, A8, A21, A23, A22, FINSEQ_1:def 13; :: thesis:

end;

set F2 = Sgm {x};
set F1 = Sgm (X \ {x});
reconsider F1 = Sgm (X \ {x}) as FinSequence of NAT ;
set a1 = Product F1;
A24: Sgm {x} = <*x*> by FINSEQ_3:44;
then A25: rng (Sgm {x}) = {x} by FINSEQ_1:39;
A26: (X \ {x}) \/ {x} = X \/ {x} by XBOOLE_1:39
.= X by A10, A13, ZFMISC_1:40 ;
then A27: F = F1 ^ (Sgm {x}) by A6, A12, A14, A15, FINSEQ_3:42;
then ( rng F c= SetPrimes & rng F1 c= rng F ) by FINSEQ_1:29, FINSEQ_1:def 4;
then A28: rng F1 c= SetPrimes by XBOOLE_1:1;
len F = (len F1) + (len (Sgm {x})) by A27, FINSEQ_1:22;
then A29: n + 1 = (len F1) + 1 by A8, A24, FINSEQ_1:39;
reconsider F1 = F1 as FinSequence of SetPrimes by A28, FINSEQ_1:def 4;

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

end;

then A30: Product F1 <> 0 by Th42;
Product F = Product (F1 ^ (Sgm {x})) by A6, A12, A14, A15, A26, FINSEQ_3:42
.= Product (F1 ^ <*x*>) by FINSEQ_3:44
.= (Product F1) * x by RVSUM_1:96 ;
then A31: p |-count a = (p |-count (Product F1)) + (p |-count x) by A7, A30, NAT_3:28;
A32: X \ {x} c= SetPrimes by A4, A11, XBOOLE_1:1;
A33: rng F1 = X \ {x} by A12, FINSEQ_1:def 13;

A34: now

assume p in rng F ; :: thesis:
then p in (rng F1) \/ (rng (Sgm {x})) by A27, FINSEQ_1:31;
then A35: ( p in rng F1 or p in {x} ) by A25, XBOOLE_0:def 3;
A36: p > 1 by INT_2:def 4;

per cases by A35, TARSKI:def 1;

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

then not p in {x} by A33, XBOOLE_0:def 5;
then p <> x by TARSKI:def 1;
then p |-count x = 0 by A36, NAT_3:24;
hence p |-count a = 1 by A3, A32, A12, A29, A31, A37; :: thesis:

end;

suppose A38: p = x ; :: thesis:

then p in {x} by TARSKI:def 1;
then not p in rng F1 by A33, XBOOLE_0:def 5;
then p |-count (Product F1) = 0 by A3, A32, A12, A29;
hence p |-count a = 1 by A31, A36, A38, NAT_3:22; :: thesis:

end;

end;

end;

assume not p in rng F ; :: thesis:
then A39: not p in (rng F1) \/ (rng (Sgm {x})) by A27, FINSEQ_1:31;
then not p in {x} by A25, XBOOLE_0:def 3;
then A40: p <> x by TARSKI:def 1;
not p in rng F1 by A39, XBOOLE_0:def 3;
then A41: p |-count (Product F1) = 0 by A3, A32, A12, A29;
p <> 1 by INT_2:def 4;
hence p |-count a = 0 by A31, A41, A40, 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 A34; :: thesis:

end;

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

end;

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 that
X c= SetPrimes and
X c= Seg k and
F = Sgm X and
A43: a = Product F and
A44: len F = 0 ; :: thesis:
A45: F = <*> REAL by A44;
assume A46: ( ( p in rng F & not p |-count a = 1 ) or ( not p in rng F & not p |-count a = 0 ) ) ; :: thesis:

per cases by A46;

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

hence contradiction by A45; :: thesis:

end;

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

F = <*> SetPrimes by A44;
then ( a = 1 & p <> 1 ) by A43, INT_2:def 4, RVSUM_1:94;
hence contradiction by A47, NAT_3:21; :: thesis:

end;

end;

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A42, A2);
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 A1; :: thesis: