let X be RealUnitarySpace; :: thesis: for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist (seq1 + seq2),(g1 + g2) is convergent & lim (dist (seq1 + seq2),(g1 + g2)) = 0 )
let g1, g2 be Point of X; :: thesis: for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist (seq1 + seq2),(g1 + g2) is convergent & lim (dist (seq1 + seq2),(g1 + g2)) = 0 )
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ( dist (seq1 + seq2),(g1 + g2) is convergent & lim (dist (seq1 + seq2),(g1 + g2)) = 0 ) )
assume that
A1: seq1 is convergent and
A2: lim seq1 = g1 and
A3: seq2 is convergent and
A4: lim seq2 = g2 ; :: thesis: ( dist (seq1 + seq2),(g1 + g2) is convergent & lim (dist (seq1 + seq2),(g1 + g2)) = 0 )
A5: seq1 + seq2 is convergent by A1, A3, Th3;
lim (seq1 + seq2) = g1 + g2 by A1, A2, A3, A4, Th13;
hence ( dist (seq1 + seq2),(g1 + g2) is convergent & lim (dist (seq1 + seq2),(g1 + g2)) = 0 ) by A5, Th24; :: thesis: verum