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