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 that
A1: seq is convergent and
A2: lim seq = g ; :: thesis: ( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
A3: - seq is convergent by A1, Th6;
lim (- seq) = - g by A1, A2, Th16;
hence ( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| ) by A3, Th21; :: thesis: verum