let f be Function of R^1 ,R^1 ; :: thesis: for g being Function of REAL ,REAL st f = g & g is continuous holds
f is continuous
let g be Function of REAL ,REAL ; :: thesis: ( f = g & g is continuous implies f is continuous )
assume that
A1: f = g and
A2: g is continuous ; :: thesis: f is continuous
for x being Point of R^1 holds f is_continuous_at x

proof

let x be Point of R^1 ; :: thesis: f is_continuous_at x
dom f = REAL by A1, FUNCT_2:def 1;
then x in dom g by A1, XREAL_0:def 1;
then g is_continuous_in x by A2, FCONT_1:def 2;
hence f is_continuous_at x by A1, Th42; :: thesis: verum

end;

hence f is continuous by TMAP_1:49; :: thesis: verum