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

( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 )

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

( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 )

let a be Real; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum