let x0 be Real; :: thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} holds
( c is convergent & lim c = x0 & h + c is convergent & lim (h + c) = x0 )
let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} holds
( c is convergent & lim c = x0 & h + c is convergent & lim (h + c) = x0 )
let c be constant Real_Sequence; :: thesis: ( rng c = {x0} implies ( c is convergent & lim c = x0 & h + c is convergent & lim (h + c) = x0 ) )
assume A1: rng c = {x0} ; :: thesis: ( c is convergent & lim c = x0 & h + c is convergent & lim (h + c) = x0 )
thus c is convergent ; :: thesis: ( lim c = x0 & h + c is convergent & lim (h + c) = x0 )
x0 in rng c by A1, TARSKI:def 1;
hence A2: lim c = x0 by SEQ_4:25; :: thesis: ( h + c is convergent & lim (h + c) = x0 )
thus h + c is convergent ; :: thesis: lim (h + c) = x0
lim h = 0 ;
hence lim (h + c) = 0 + x0 by A2, SEQ_2:6
.= x0 ;
:: thesis: verum