let x0 be Real; :: thesis: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} holds
( c is convergent & lim c = x0 & h + c is convergent & lim (h + c) = x0 )
let h be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {x0} holds
( c is convergent & lim c = x0 & h + c is convergent & lim (h + c) = x0 )
let c be V8() 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:40; :: thesis: ( h + c is convergent & lim (h + c) = x0 )
A3: h is convergent by FDIFF_1:def 1;
hence h + c is convergent by SEQ_2:19; :: thesis: lim (h + c) = x0
lim h = 0 by FDIFF_1:def 1;
hence lim (h + c) = 0 + x0 by A2, A3, SEQ_2:20
.= x0 ;
:: thesis: verum