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 A1: ( 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 A2: f is_continuous_in x0 ; :: thesis: f | REAL is continuous
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

A3: now :: thesis: for x1, x2 being real number holds g /. (x1 + x2) = (g /. x1) + (g /. x2)

let x1, x2 be real number ; :: thesis: g /. (x1 + x2) = (g /. x1) + (g /. x2)
A4: ( 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 A1
.= (g /. x1) + (g /. x2) by A4, REAL_NS1:2 ; :: thesis: verum

end;

g is_continuous_in x0 by A2, Th1;
then g | REAL is continuous by A1, A3, NFCONT_3:23;
hence f | REAL is continuous by Th23; :: thesis: verum