let n be Element of NAT ; :: thesis: for f being PartFunc of (REAL n),REAL
for h being PartFunc 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 (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 (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 A1: ( 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 (REAL-NS n),REAL st
( x0 = y1 & f = g & g is_continuous_in y1 ) by Def4;
hence h is_continuous_in y0 by A1; :: thesis: verum

end;

thus ( h is_continuous_in y0 implies f is_continuous_in x0 ) by A1, Def4; :: thesis: verum