defpred S₁[ object , object ] means for k being non zero Nat st k = $1 holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
$2 = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s));
A1: for z being Nat st z in Seg s holds
ex x being Element of NAT st S₁[z,x]

proof

let z be Nat; :: thesis: ( z in Seg s implies ex x being Element of NAT st S₁[z,x] )
assume A2: z in Seg s ; :: thesis: ex x being Element of NAT st S₁[z,x]
reconsider z = z as non zero Nat by A2, FINSEQ_1:1;
z <= s by A2, FINSEQ_1:1;
then z - 1 < s - 0 by XREAL_1:8;
then reconsider e = (Product (PrimeNumbersFS s)) / (primenumber (z - 1)) as Nat by Th45;
reconsider x = (CRT (0,e,(- 1),(primenumber (z - 1)))) + (Product (PrimeNumbersFS s)) as Element of NAT by ORDINAL1:def 12;
take x ; :: thesis: S₁[z,x]
thus S₁[z,x] ; :: thesis: verum

end;

consider p being FinSequence of NAT such that
A3: dom p = Seg s and
A4: for k being Nat st k in Seg s holds
S₁[k,p . k] from FINSEQ_1:sch 5(A1);
take p ; :: thesis: ( len p = s & ( for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
p . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ) )
s in NAT by ORDINAL1:def 12;
hence len p = s by A3, FINSEQ_1:def 3; :: thesis: for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
p . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s))
let k be non zero Nat; :: thesis: ( k <= s implies for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
p . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) )
assume A5: k <= s ; :: thesis: for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
p . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s))
1 <= k by NAT_1:14;
then k in Seg s by A5;
hence for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
p . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) by A4; :: thesis: verum