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;
then g is_continuous_in x by A2;
hence f is_continuous_at x by A1, Th21; :: thesis: verum

end;

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