let X be ComplexUnitarySpace; :: thesis: for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq + x is Cauchy
let x be Point of X; :: thesis: for seq being sequence of X st seq is Cauchy holds
seq + x is Cauchy
let seq be sequence of X; :: thesis: ( seq is Cauchy implies seq + x is Cauchy )
assume A1: seq is Cauchy ; :: thesis: seq + x is Cauchy
let r be Real; :: according to CLVECT_2:def 8 :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((seq + x) . n),((seq + x) . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((seq + x) . n),((seq + x) . m)) < r
then consider m1 being Nat such that
A2: for n, m being Nat st n >= m1 & m >= m1 holds
dist ((seq . n),(seq . m)) < r by A1;
take k = m1; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist (((seq + x) . n),((seq + x) . m)) < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist (((seq + x) . n),((seq + x) . m)) < r )
dist (((seq . n) + x),((seq . m) + x)) <= (dist ((seq . n),(seq . m))) + (dist (x,x)) by CSSPACE:56;
then A3: dist (((seq . n) + x),((seq . m) + x)) <= (dist ((seq . n),(seq . m))) + 0 by CSSPACE:50;
assume ( n >= k & m >= k ) ; :: thesis: dist (((seq + x) . n),((seq + x) . m)) < r
then dist ((seq . n),(seq . m)) < r by A2;
then dist (((seq . n) + x),((seq . m) + x)) < r by A3, XXREAL_0:2;
then dist (((seq + x) . n),((seq . m) + x)) < r by BHSP_1:def 6;
hence dist (((seq + x) . n),((seq + x) . m)) < r by BHSP_1:def 6; :: thesis: verum