let m, n be non zero Nat; :: thesis:
let f be PartFunc of (REAL m),(REAL n); :: thesis:
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis:
let X be set ; :: thesis:
assume A1: f = g ; :: thesis:

hereby :: thesis:

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

let y0 be Point of (REAL-NS m); :: thesis:
assume A4: y0 in X ; :: thesis:
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:

end;

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

end;

assume A5: g is_continuous_on X ; :: thesis:
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;

let x0 be Element of REAL m; :: thesis:
assume A7: x0 in X ; :: thesis:
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:

end;

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