Sorry Piotr, I accidentally press the 'Send' button.
The environment needed (maybe it could be shorter, so rather sufficient) for the proof in the previous message:
vocabulary RLVECT_1, FINSEQ_2, FINSEQ_1, ARYTM_3;
constructors REAL_1,NAT_1,FINSEQ_2,RVSUM_1,NEWTON;
notation ARYTM,REAL_1,NAT_1,FINSEQ_1,FINSEQ_2,NEWTON,RVSUM_1;
clusters ARYTM_3, NAT_1, ARYTM;
theorems FINSEQ_2,AXIOMS,RVSUM_1,REAL_1, REAL_2;
schemes NAT_1;
requirements BOOLE,SUBSET,ARYTM,REAL;
Greetings,
Andrzej