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) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )
let g be Point of X; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 ) )
assume that
A1: seq is convergent and
A2: lim seq = g ; :: thesis: ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )
A3: - seq is convergent by A1, Th6;
lim (- seq) = - g by A1, A2, Th16;
hence ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 ) by A3, Th22; :: thesis: verum