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 that
A1: seq1 is convergent and
A2: lim seq1 = g1 and
A3: seq2 is convergent and
A4: lim seq2 = g2 ; :: thesis: ( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| )
A5: seq1 - seq2 is convergent by A1, A3, Th4;
lim (seq1 - seq2) = g1 - g2 by A1, A2, A3, A4, Th14;
hence ( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| ) by A5, Th21; :: thesis: verum