let f, g be FinSequence of NAT ; :: thesis: ( len f = s & ( for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
f . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ) & len g = s & ( for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
g . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ) implies f = g )
assume that
A6: len f = s and
A7: for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
f . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) and
A8: len g = s and
A9: for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
g . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ; :: thesis: f = g
thus len f = len g by A6, A8; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len f or f . b₁ = g . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len f or f . k = g . k )
assume that
A10: 1 <= k and
A11: k <= len f ; :: thesis: f . k = g . k
reconsider k1 = k - 1 as Element of NAT by A10, INT_1:3;
k - 1 < s - 0 by A6, A11, XREAL_1:8;
then reconsider e = (Product (PrimeNumbersFS s)) / (primenumber k1) as Nat by Th45;
thus f . k = (CRT (0,e,(- 1),(primenumber k1))) + (Product (PrimeNumbersFS s)) by A6, A7, A10, A11
.= g . k by A6, A9, A10, A11 ; :: thesis: verum