let n be Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) st f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 holds
f | REAL is continuous
let f be PartFunc of REAL,(REAL n); :: thesis: ( f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 implies f | REAL is continuous )
assume AS: ( f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) ) ; :: thesis: ( for x0 being real number holds not f is_continuous_in x0 or f | REAL is continuous )
given x0 being real number such that P3: f is_continuous_in x0 ; :: thesis: f | REAL is continuous
reconsider g = f as PartFunc of REAL, the carrier of (REAL-NS n) by REAL_NS1:def 4;

P2: now

let x1, x2 be real number ; :: thesis: g /. (x1 + x2) = (g /. x1) + (g /. x2)
P21: ( g /. x1 = f /. x1 & g /. x2 = f /. x2 ) by REAL_NS1:def 4;
thus g /. (x1 + x2) = f /. (x1 + x2) by REAL_NS1:def 4
.= (f /. x1) + (f /. x2) by AS
.= (g /. x1) + (g /. x2) by P21, REAL_NS1:2 ; :: thesis: verum

end;

g is_continuous_in x0 by P3, Def1Th;
then g | REAL is continuous by AS, P2, NFCONT_3:23;
hence f | REAL is continuous by Def2Th; :: thesis: verum