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