let X be RealUnitarySpace; :: 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 BHSP_3:def 1 :: thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq + x) . n),((seq + x) . m) < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq + x) . n),((seq + x) . m) < r
then consider m1 being Element of NAT such that
A2: for n, m being Element of NAT st n >= m1 & m >= m1 holds
dist (seq . n),(seq . m) < r by A1, Def1;
take k = m1; :: thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq + x) . n),((seq + x) . m) < r
let n, m be Element of NAT ; :: thesis: ( n >= k & m >= k implies dist ((seq + x) . n),((seq + x) . m) < r )
assume ( n >= k & m >= k ) ; :: thesis: dist ((seq + x) . n),((seq + x) . m) < r
then A3: dist (seq . n),(seq . m) < r by A2;
dist ((seq . n) + x),((seq . m) + x) <= (dist (seq . n),(seq . m)) + (dist x,x) by BHSP_1:47;
then dist ((seq . n) + x),((seq . m) + x) <= (dist (seq . n),(seq . m)) + 0 by BHSP_1:41;
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 12;
hence dist ((seq + x) . n),((seq + x) . m) < r by BHSP_1:def 12; :: thesis: verum