let h be Function of T,(TOP-REAL n); :: thesis: ( h = f [+] r implies h is continuous )

assume A1: h = f [+] r ; :: thesis: h is continuous

reconsider r = r as Element of R^1 by XREAL_0:def 1;

dom f = the carrier of T by FUNCT_2:def 1;

then h = f <+> (T --> r) by A1, Th29;

hence h is continuous ; :: thesis: verum

assume A1: h = f [+] r ; :: thesis: h is continuous

reconsider r = r as Element of R^1 by XREAL_0:def 1;

dom f = the carrier of T by FUNCT_2:def 1;

then h = f <+> (T --> r) by A1, Th29;

hence h is continuous ; :: thesis: verum