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