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

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