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

proof

let x0 be real number ; :: thesis: ( x0 in dom (g | REAL ) implies g | REAL is_continuous_in x0 )
assume x0 in dom (g | REAL ) ; :: thesis: g | REAL is_continuous_in x0
reconsider x0 = x0 as Real by XREAL_0:def 1;
reconsider x1 = x0 as Point of R^1 by TOPMETR:24;
A3: f is_continuous_at x1 by TMAP_1:49;
dom g c= REAL ;
then f = g | REAL by A2, RELAT_1:97;
hence g | REAL is_continuous_in x0 by A3, Th7; :: thesis: verum

end;

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