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

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