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