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 A1: ( f in Big_Oh g & g in Big_Oh h ) ; :: thesis: f in Big_Oh h
then Big_Oh g c= Big_Oh h by Th11;
hence f in Big_Oh h by A1; :: thesis: verum