let X be ComplexUnitarySpace; :: thesis: for seq1, seq2, seq being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 + seq2 holds
seq is constant
let seq1, seq2, seq be sequence of X; :: thesis: ( seq1 is constant & seq2 is constant & seq = seq1 + seq2 implies seq is constant )
assume that
A1: seq1 is constant and
A2: seq2 is constant and
A3: seq = seq1 + seq2 ; :: thesis: seq is constant
consider x being Point of X such that
A4: for n being Nat holds seq1 . n = x by A1, VALUED_0:def 18;
consider y being Point of X such that
A5: for n being Nat holds seq2 . n = y by A2, VALUED_0:def 18;
take z = x + y; :: 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 = (seq1 . n) + (seq2 . n) by A3, NORMSP_1:def 5
.= x + (seq2 . n) by A4
.= z by A5 ;
:: thesis: verum