let r be Real; :: thesis: for seq, seq1 being Real_Sequence st seq is convergent & ( for n being Nat holds seq1 . n = r - (seq . n) ) holds
( seq1 is convergent & lim seq1 = r - (lim seq) )
let seq, seq1 be Real_Sequence; :: thesis: ( seq is convergent & ( for n being Nat holds seq1 . n = r - (seq . n) ) implies ( seq1 is convergent & lim seq1 = r - (lim seq) ) )
assume that
A1: seq is convergent and
A2: for n being Nat holds seq1 . n = r - (seq . n) ; :: thesis: ( seq1 is convergent & lim seq1 = r - (lim seq) )
consider r1 being Real such that
A3: for r2 being Real st 0 < r2 holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r1).| < r2 by A1, SEQ_2:def 6;

A4: now :: thesis: for r2 being Real st 0 < r2 holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (r - r1)).| < r2

let r2 be Real; :: thesis: ( 0 < r2 implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (r - r1)).| < r2 )
assume 0 < r2 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (r - r1)).| < r2
then consider n being Nat such that
A5: for m being Nat st n <= m holds
|.((seq . m) - r1).| < r2 by A3;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((seq1 . m) - (r - r1)).| < r2

now :: thesis: for m being Nat st n <= m holds
|.((seq1 . m) - (r - r1)).| < r2

let m be Nat; :: thesis: ( n <= m implies |.((seq1 . m) - (r - r1)).| < r2 )
assume A6: n <= m ; :: thesis: |.((seq1 . m) - (r - r1)).| < r2
|.((seq . m) - r1).| = |.(- ((seq . m) - r1)).| by COMPLEX1:52
.= |.((r1 - r) + (r - (seq . m))).|
.= |.((seq1 . m) + (- (- (r1 - r)))).| by A2
.= |.((seq1 . m) - (r - r1)).| ;
hence |.((seq1 . m) - (r - r1)).| < r2 by A5, A6; :: thesis: verum

end;

hence for m being Nat st n <= m holds
|.((seq1 . m) - (r - r1)).| < r2 ; :: thesis: verum

end;

hence A7: seq1 is convergent by SEQ_2:def 6; :: thesis: lim seq1 = r - (lim seq)
lim seq = r1 by A1, A3, SEQ_2:def 7;
hence lim seq1 = r - (lim seq) by A4, A7, SEQ_2:def 7; :: thesis: verum