let X be ComplexUnitarySpace; :: thesis: for seq, seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 + seq2 holds
seq is constant
let seq, seq1, seq2 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;
consider y being Point of X such that
A5: for n being Nat holds seq2 . n = y by A2;
take z = x + y; :: according to VALUED_0:def 20 :: thesis: for b₁ being set holds seq . b₁ = z
let n be Nat; :: thesis: seq . n = z
thus seq . n = (seq1 . n) + (seq2 . n) by A3, NORMSP_1:def 2
.= x + (seq2 . n) by A4
.= z by A5 ; :: thesis: verum