let X be non empty strict SubSpace of R^1 ; :: thesis: for f being RealMap of X
for g being PartFunc of REAL,REAL st g = f holds
( f is continuous iff g is continuous )
let f be RealMap of X; :: thesis: for g being PartFunc of REAL,REAL st g = f holds
( f is continuous iff g is continuous )
let g be PartFunc of REAL,REAL; :: thesis: ( g = f implies ( f is continuous iff g is continuous ) )
assume A1: g = f ; :: thesis: ( f is continuous iff g is continuous )
A2: dom g = the carrier of X by FUNCT_2:def 1, A1;

hereby :: thesis: ( g is continuous implies f is continuous )

assume B3: f is continuous ; :: thesis: g is continuous
for x0 being Real st x0 in dom g holds
g is_continuous_in x0

proof

let x0 be Real; :: thesis: ( x0 in dom g implies g is_continuous_in x0 )
assume x0 in dom g ; :: thesis: g is_continuous_in x0
then reconsider x = x0 as Point of X by FUNCT_2:def 1, A1;
for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) by B3, C0SP2:1;
hence g is_continuous_in x0 by A1, Th80a; :: thesis: verum

end;

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

end;

assume B5: g is continuous ; :: thesis: f is continuous
for x being Point of X
for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V )

proof

let x be Point of X; :: thesis: for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V )
let V be Subset of REAL; :: thesis: ( f . x in V & V is open implies ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )
assume A6: ( f . x in V & V is open ) ; :: thesis: ex W being Subset of X st
( x in W & W is open & f .: W c= V )
reconsider x0 = x as Real ;
g is_continuous_in x0 by B5, FCONT_1:def 2, A2;
hence ex W being Subset of X st
( x in W & W is open & f .: W c= V ) by A1, A6, Th80a; :: thesis: verum

end;

hence f is continuous by C0SP2:1; :: thesis: verum