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;

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

( 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

hence A7:
seq1 is convergent
by SEQ_2:def 6; :: thesis: lim seq1 = r - (lim seq)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

|.((seq1 . m) - (r - r1)).| < r2 ; :: thesis: verum

end;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

hence
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;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

|.((seq1 . m) - (r - r1)).| < r2 ; :: thesis: verum

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