let n be Element of NAT ; :: thesis: for f being PartFunc of (REAL n),REAL
for h being PartFunc of the carrier of (REAL-NS n),REAL
for x0 being Element of REAL n
for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
let f be PartFunc of (REAL n),REAL; :: thesis: for h being PartFunc of the carrier of (REAL-NS n),REAL
for x0 being Element of REAL n
for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
let h be PartFunc of the carrier of (REAL-NS n),REAL; :: thesis: for x0 being Element of REAL n
for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
let x0 be Element of REAL n; :: thesis: for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
let y0 be Point of (REAL-NS n); :: thesis: ( f = h & x0 = y0 implies ( f is_continuous_in x0 iff h is_continuous_in y0 ) )
assume AS: ( f = h & x0 = y0 ) ; :: thesis: ( f is_continuous_in x0 iff h is_continuous_in y0 )

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

assume f is_continuous_in x0 ; :: thesis: h is_continuous_in y0
then ex y1 being Point of (REAL-NS n) ex g being PartFunc of the carrier of (REAL-NS n),REAL st
( x0 = y1 & f = g & g is_continuous_in y1 ) by XDef1a;
hence h is_continuous_in y0 by AS; :: thesis: verum

end;

thus ( h is_continuous_in y0 implies f is_continuous_in x0 ) by AS, XDef1a; :: thesis: verum