theorem :: BHSP_3:40

for X being RealUnitarySpace
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