set f = sequenceA s;
let m be Nat; :: according to RVSUM_3:def 1 :: thesis: ( not m in dom (sequenceA s) or not (sequenceA s) . m <= 0 )
assume A1: m in dom (sequenceA s) ; :: thesis: not (sequenceA s) . m <= 0
then reconsider m = m as non zero Nat by FINSEQ_3:25;
A2: len (sequenceA s) = s by Def5;
A3: m <= len (sequenceA s) by A1, FINSEQ_3:25;
m - 1 < m - 0 by XREAL_1:8;
then m - 1 < s by A2, A3, XXREAL_0:2;
then reconsider e = (Product (PrimeNumbersFS s)) / (primenumber (m - 1)) as Nat by Th45;
(sequenceA s) . m = (CRT (0,e,(- 1),(primenumber (m - 1)))) + (Product (PrimeNumbersFS s)) by A2, A3, Def5;
hence not (sequenceA s) . m <= 0 ; :: thesis: verum