let t be Real; :: thesis: for f being convergent Real_Sequence holds lim (t + f) = t + (lim f)
let f be convergent Real_Sequence; :: thesis: lim (t + f) = t + (lim f)
reconsider r = t as Element of REAL by XREAL_0:def 1;
f + (NAT --> t) = t + f by Th5;
hence lim (t + f) = (lim (NAT --> r)) + (lim f) by SEQ_2:6
.= t + (lim f) by Th6 ;
:: thesis: verum