let X be ComplexUnitarySpace; :: thesis: for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
let g be Point of X; :: thesis: for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
let z be Complex; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 ) )
assume ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
then ( z * seq is convergent & lim (z * seq) = z * g ) by Th5, Th15;
hence ( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 ) by Th22; :: thesis: verum