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 ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )

then ( - seq is convergent & lim (- seq) = - g ) by Th6, Th16;

hence ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 ) by Th22; :: thesis: verum

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 ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )

then ( - seq is convergent & lim (- seq) = - g ) by Th6, Th16;

hence ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 ) by Th22; :: thesis: verum