let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set st f = g holds
( f is_continuous_on X iff g is_continuous_on X )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set st f = g holds
( f is_continuous_on X iff g is_continuous_on X )
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for X being set st f = g holds
( f is_continuous_on X iff g is_continuous_on X )
let X be set ; :: thesis: ( f = g implies ( f is_continuous_on X iff g is_continuous_on X ) )
assume A1: f = g ; :: thesis: ( f is_continuous_on X iff g is_continuous_on X )

hereby :: thesis: ( g is_continuous_on X implies f is_continuous_on X )

assume A2: f is_continuous_on X ; :: thesis: g is_continuous_on X
then A3: ( X c= dom f & ( for x0 being Element of REAL m st x0 in X holds
f | X is_continuous_in x0 ) ) ;

now :: thesis: for y0 being Point of (REAL-NS m) st y0 in X holds
g | X is_continuous_in y0

let y0 be Point of (REAL-NS m); :: thesis: ( y0 in X implies g | X is_continuous_in y0 )
assume A4: y0 in X ; :: thesis: g | X is_continuous_in y0
reconsider x0 = y0 as Element of REAL m by REAL_NS1:def 4;
f | X is_continuous_in x0 by A2, A4;
hence g | X is_continuous_in y0 by A1; :: thesis: verum

end;

hence g is_continuous_on X by A3, A1, NFCONT_1:def 7; :: thesis: verum

end;

assume A5: g is_continuous_on X ; :: thesis: f is_continuous_on X
then A6: ( X c= dom g & ( for y0 being Point of (REAL-NS m) st y0 in X holds
g | X is_continuous_in y0 ) ) by NFCONT_1:def 7;

now :: thesis: for x0 being Element of REAL m st x0 in X holds
f | X is_continuous_in x0

let x0 be Element of REAL m; :: thesis: ( x0 in X implies f | X is_continuous_in x0 )
assume A7: x0 in X ; :: thesis: f | X is_continuous_in x0
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;
g | X is_continuous_in y0 by A5, A7, NFCONT_1:def 7;
hence f | X is_continuous_in x0 by A1; :: thesis: verum

end;

hence f is_continuous_on X by A6, A1; :: thesis: verum