let h be Function of T,(TOP-REAL n); :: thesis: ( h = f <#> g implies h is continuous )
assume A3: h = f <#> g ; :: thesis: h is continuous
reconsider G = f <##> (incl (g,n)) as Function of T,(TOP-REAL n) by Th41;
h = G by A3, Th51;
hence h is continuous ; :: thesis: verum