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
( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
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
( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| ) )
assume ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 ) ; :: thesis: ( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
then ( seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 ) by Th3, Th13;
hence ( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| ) by Th21; :: thesis: verum