let f, g, h be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Theta g & g in Big_Theta h implies f in Big_Theta h )
assume that
A1:
f in Big_Theta g
and
A2:
g in Big_Theta h
; :: thesis: f in Big_Theta h
A3:
( f in Big_Oh g & f in Big_Omega g )
by A1, XBOOLE_0:def 4;
A4:
( g in Big_Oh h & g in Big_Omega h )
by A2, XBOOLE_0:def 4;
then A5:
f in Big_Oh h
by A3, Th12;
f in Big_Omega h
by A3, A4, Th21;
hence
f in Big_Theta h
by A5, XBOOLE_0:def 4; :: thesis: verum