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

reconsider g1 = g " as Function of T,R^1 ;

g1 is continuous ;

hence ( h = f </> g implies h is continuous ) ; :: thesis: verum