reconsider r = t as Element of 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 ; :: thesis: verum