let h be Function of T,(TOP-REAL n); :: thesis: ( h = f </> g implies h is continuous )
reconsider g1 = g " as Function of T,R^1 ;
g1 is continuous ;
hence ( h = f </> g implies h is continuous ) ; :: thesis: verum