let X be ComplexUnitarySpace; :: thesis: for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
let g, x be Point of X; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| ) )
assume ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
then ( ||.(seq + (- x)).|| is convergent & lim ||.(seq + (- x)).|| = ||.(g + (- x)).|| ) by Lm1;
then ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g + (- x)).|| ) by CSSPACE:78;
hence ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| ) by RLVECT_1:def 12; :: thesis: verum