- s2 is convergent ;
hence for b₁ being Complex_Sequence st b₁ = s1 - s2 holds
b₁ is convergent ; :: thesis: verum