let f, g, h be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Oh g & g in Big_Oh h implies f in Big_Oh h )
assume that
A1: f in Big_Oh g and
A2: g in Big_Oh h ; :: thesis: f in Big_Oh h
Big_Oh g c= Big_Oh h by A2, Th11;
hence f in Big_Oh h by A1; :: thesis: verum