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 ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 ) ; :: thesis: ( dist ((seq1 - seq2),(g1 - g2)) is convergent & lim (dist ((seq1 - seq2),(g1 - g2))) = 0 )
then ( seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 ) by Th4, Th14;
hence ( dist ((seq1 - seq2),(g1 - g2)) is convergent & lim (dist ((seq1 - seq2),(g1 - g2))) = 0 ) by Th24; :: thesis: verum