let r be Real; :: thesis: for seq, seq1 being Real_Sequence st seq is convergent & ( for n being Element of 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 Element of 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 Element of NAT holds seq1 . n = r - (seq . n) ; :: thesis: ( seq1 is convergent & lim seq1 = r - (lim seq) )
consider r1 being real number such that
A3: for r2 being real number st 0 < r2 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r1) < r2 by A1, SEQ_2:def 6;

A4: now

let r2 be real number ; :: thesis: ( 0 < r2 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (r - r1)) < r2 )
assume 0 < r2 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (r - r1)) < r2
then consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
abs ((seq . m) - r1) < r2 by A3;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (r - r1)) < r2

now

let m be Element of NAT ; :: thesis: ( n <= m implies abs ((seq1 . m) - (r - r1)) < r2 )
assume A6: n <= m ; :: thesis: abs ((seq1 . m) - (r - r1)) < r2
abs ((seq . m) - r1) = abs (- ((seq . m) - r1)) by COMPLEX1:138
.= abs ((r1 - r) + (r - (seq . m)))
.= abs ((seq1 . m) + (- (- (r1 - r)))) by A2
.= abs ((seq1 . m) - (r - r1)) ;
hence abs ((seq1 . m) - (r - r1)) < r2 by A5, A6; :: thesis: verum

end;

hence for m being Element of NAT st n <= m holds
abs ((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