let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X
for k being Nat st seq1 is_compared_to seq2 holds
seq1 ^\ k is_compared_to seq2 ^\ k
let seq1, seq2 be sequence of X; :: thesis: for k being Nat st seq1 is_compared_to seq2 holds
seq1 ^\ k is_compared_to seq2 ^\ k
let k be Nat; :: thesis: ( seq1 is_compared_to seq2 implies seq1 ^\ k is_compared_to seq2 ^\ k )
assume A1: seq1 is_compared_to seq2 ; :: thesis: seq1 ^\ k is_compared_to seq2 ^\ k
let r be Real; :: according to BHSP_3:def 2 :: thesis: ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r )
assume r > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r
then consider m1 being Nat such that
A2: for n being Nat st n >= m1 holds
dist ((seq1 . n),(seq2 . n)) < r by A1;
take m = m1; :: thesis: for n being Nat st n >= m holds
dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r
let n be Nat; :: thesis: ( n >= m implies dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r )
assume A3: n >= m ; :: thesis: dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r
n + k >= n by NAT_1:11;
then n + k >= m by A3, XXREAL_0:2;
then dist ((seq1 . (n + k)),(seq2 . (n + k))) < r by A2;
then dist (((seq1 ^\ k) . n),(seq2 . (n + k))) < r by NAT_1:def 3;
hence dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r by NAT_1:def 3; :: thesis: verum