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

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