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 )

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 A2:
f is continuous
; :: thesis: 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;then for x0 being Real st x0 in dom f holds

f is_continuous_in x0 by A1;

hence f is continuous ; :: thesis: verum

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

g is_continuous_in x0

hence
g is continuous
; :: thesis: verumg 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;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