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 st x0 in dom g holds
g is_continuous_in x0 by A1, Th6, TMAP_1:44, TOPMETR:17;
hence g is continuous by FCONT_1:def 2; :: thesis: verum