let f be continuous Function of R^1,R^1; :: thesis: for g being PartFunc of REAL,REAL st f = g holds
g is continuous
let g be PartFunc of REAL,REAL; :: thesis: ( f = g implies g is continuous )
assume A1: f = g ; :: thesis: g is continuous
for x0 being real number st x0 in dom g holds
g is_continuous_in x0

proof

let x0 be real number ; :: thesis: ( x0 in dom g implies g is_continuous_in x0 )
assume x0 in dom g ; :: thesis: g is_continuous_in x0
reconsider x0 = x0 as Real by XREAL_0:def 1;
reconsider x1 = x0 as Point of R^1 by TOPMETR:17;
f is_continuous_at x1 by TMAP_1:44;
hence g is_continuous_in x0 by A1, Th7; :: thesis: verum

end;

hence g is continuous by FCONT_1:def 2; :: thesis: verum