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).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
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).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
let z be Complex; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| ) )
assume that
A1: seq is convergent and
A2: lim seq = g ; :: thesis: ( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
A3: z * seq is convergent by A1, Th5;
lim (z * seq) = z * g by A1, A2, Th15;
hence ( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| ) by A3, Th21; :: thesis: verum