let X be Banach_Algebra; :: thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X holds
lim seq1 = lim seq2
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X implies lim seq1 = lim seq2 )
assume that
A1: seq1 is convergent and
A2: seq2 is convergent and
A3: lim (seq1 - seq2) = 0. X ; :: thesis: lim seq1 = lim seq2
(lim seq1) - (lim seq2) = 0. X by A1, A2, A3, NORMSP_1:26;
then ((lim seq1) - (lim seq2)) + (lim seq2) = lim seq2 by LOPBAN_3:38;
then (lim seq1) - ((lim seq2) - (lim seq2)) = lim seq2 by LOPBAN_3:38;
then (lim seq1) - (0. X) = lim seq2 by RLVECT_1:15;
hence lim seq1 = lim seq2 by RLVECT_1:13; :: thesis: verum