for F being eventually-nonnegative Real_Sequence st F = (seq_n^ 1) - (seq_const 1) holds
(Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1)