let n be Element of NAT ; :: thesis: for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of REAL,(REAL n) st g = f holds
( g is continuous iff f is continuous )
let g be PartFunc of REAL,(REAL-NS n); :: thesis: for f being PartFunc of REAL,(REAL n) st g = f holds
( g is continuous iff f is continuous )
let f be PartFunc of REAL,(REAL n); :: thesis: ( g = f implies ( g is continuous iff f is continuous ) )
assume A1: g = f ; :: thesis: ( g is continuous iff f is continuous )

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

assume g is continuous ; :: thesis: f is continuous
then for x0 being Real st x0 in dom f holds
f is_continuous_in x0 by A1;
hence f is continuous ; :: thesis: verum

end;

assume A2: f is continuous ; :: thesis: g is continuous

now :: thesis: for x0 being Real st x0 in dom g holds
g is_continuous_in x0

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 f is_continuous_in x0 by A2, A1;
hence g is_continuous_in x0 by A1; :: thesis: verum

end;

hence g is continuous ; :: thesis: verum