for f, g being eventually-nonnegative Real_Sequence holds max ((Big_Oh f),(Big_Oh g)) = Big_Oh (max (f,g))