let a be Complex; :: thesis: for X being ComplexUnitarySpace
for seq1, seq being sequence of X st seq1 is constant & seq = a * seq1 holds
seq is constant
let X be ComplexUnitarySpace; :: thesis: for seq1, seq being sequence of X st seq1 is constant & seq = a * seq1 holds
seq is constant
let seq1, seq be sequence of X; :: thesis: ( seq1 is constant & seq = a * seq1 implies seq is constant )
assume that
A1: seq1 is constant and
A2: seq = a * seq1 ; :: thesis: seq is constant
consider x being Point of X such that
A3: for n being Nat holds seq1 . n = x by A1, VALUED_0:def 18;
take z = a * x; :: according to VALUED_0:def 18 :: thesis: for b₁ being set holds seq . b₁ = z
let n be Nat; :: thesis: seq . n = z
n in NAT by ORDINAL1:def 13;
hence seq . n = a * (seq1 . n) by A2, CLVECT_1:def 15
.= z by A3 ;
:: thesis: verum