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 Th4, Th14;

hence ( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| ) by Th21; :: thesis: verum

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 Th4, Th14;

hence ( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| ) by Th21; :: thesis: verum