reconsider r = t as Real by XREAL_0:def 1;
f + (NAT --> r) = t + f by Th5;
hence for b₁ being Real_Sequence st b₁ = t + f holds
b₁ is convergent by SEQ_2:5; :: thesis: verum