let X be RealUnitarySpace; :: thesis: for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
let g be Point of X; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| ) )
assume ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
then ( - seq is convergent & lim (- seq) = - g ) by Th6, Th16;
hence ( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| ) by Th21; :: thesis: verum