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

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