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

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

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

end;

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