let n be Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) st f is total & ( for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Real 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 holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Real st f is_continuous_in x0 implies f | REAL is continuous )

assume A1: ( f is total & ( for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) ) ; :: thesis: ( for x0 being Real holds not f is_continuous_in x0 or f | REAL is continuous )

given x0 being Real 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;

then g | REAL is continuous by A1, A3, NFCONT_3:23;

hence f | REAL is continuous by Th23; :: thesis: verum

f | REAL is continuous

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is total & ( for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Real st f is_continuous_in x0 implies f | REAL is continuous )

assume A1: ( f is total & ( for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) ) ; :: thesis: ( for x0 being Real holds not f is_continuous_in x0 or f | REAL is continuous )

given x0 being Real 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 holds g /. (x1 + x2) = (g /. x1) + (g /. x2)

g is_continuous_in x0
by A2;let x1, x2 be Real; :: 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;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

then g | REAL is continuous by A1, A3, NFCONT_3:23;

hence f | REAL is continuous by Th23; :: thesis: verum