:: deftheorem Def5 defines sequenceA NUMBER15:def 5 :
for s being Nat
for b₂ being FinSequence of NAT holds
( b₂ = sequenceA s iff ( len b₂ = s & ( for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
b₂ . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ) ) );