let X be RealUnitarySpace; :: thesis: for f being Function of X,REAL
for g being Function of (RUSp2RNSp X),REAL
for x0 being Point of X
for y0 being Point of (RUSp2RNSp X) st f = g & x0 = y0 holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let f be Function of X,REAL; :: thesis: for g being Function of (RUSp2RNSp X),REAL
for x0 being Point of X
for y0 being Point of (RUSp2RNSp X) st f = g & x0 = y0 holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let g be Function of (RUSp2RNSp X),REAL; :: thesis: for x0 being Point of X
for y0 being Point of (RUSp2RNSp X) st f = g & x0 = y0 holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let x0 be Point of X; :: thesis: for y0 being Point of (RUSp2RNSp X) st f = g & x0 = y0 holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let y0 be Point of (RUSp2RNSp X); :: thesis: ( f = g & x0 = y0 implies ( f is_continuous_in x0 iff g is_continuous_in y0 ) )
assume AS: ( f = g & x0 = y0 ) ; :: thesis: ( f is_continuous_in x0 iff g is_continuous_in y0 )
set Y = RUSp2RNSp X;

hereby :: thesis: ( g is_continuous_in y0 implies f is_continuous_in x0 )

assume A11: f is_continuous_in x0 ; :: thesis: g is_continuous_in y0
for s2 being sequence of (RUSp2RNSp X) st rng s2 c= dom g & s2 is convergent & lim s2 = y0 holds
( g /* s2 is convergent & g /. y0 = lim (g /* s2) )

proof

let s2 be sequence of (RUSp2RNSp X); :: thesis: ( rng s2 c= dom g & s2 is convergent & lim s2 = y0 implies ( g /* s2 is convergent & g /. y0 = lim (g /* s2) ) )
assume AS1: ( rng s2 c= dom g & s2 is convergent & lim s2 = y0 ) ; :: thesis: ( g /* s2 is convergent & g /. y0 = lim (g /* s2) )
reconsider s1 = s2 as sequence of X ;
B2: s1 is convergent by AS1, RHS8;
then lim s1 = x0 by AS1, AS, RHS9;
hence ( g /* s2 is convergent & g /. y0 = lim (g /* s2) ) by AS, A11, AS1, B2; :: thesis: verum

end;

hence g is_continuous_in y0 by A11, AS; :: thesis: verum

end;

assume A31: g is_continuous_in y0 ; :: thesis: f is_continuous_in x0
for s1 being sequence of X st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) )

proof

let s1 be sequence of X; :: thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )
assume AS2: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 ) ; :: thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
reconsider s2 = s1 as sequence of (RUSp2RNSp X) ;
B2: s2 is convergent by AS2, RHS8;
lim s2 = y0 by AS, AS2, RHS9;
hence ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by AS, A31, AS2, B2; :: thesis: verum

end;

hence f is_continuous_in x0 by A31, AS; :: thesis: verum