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