let n be Element of NAT ; :: thesis: for X being set
for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st ( for x0 being Real st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let X be set ; :: thesis: for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st ( for x0 being Real st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let f be PartFunc of REAL,(REAL n); :: thesis: for r, p being Element of REAL n st ( for x0 being Real st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let r, p be Element of REAL n; :: thesis: ( ( for x0 being Real st x0 in X holds
f /. x0 = (x0 * r) + p ) implies f | X is continuous )
assume A1: for x0 being Real st x0 in X holds
f /. x0 = (x0 * r) + p ; :: thesis: f | X is continuous
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
reconsider r0 = r, p0 = p as Point of (REAL-NS n) by REAL_NS1:def 4;

now :: thesis: for x0 being Real st x0 in X holds
g /. x0 = (x0 * r0) + p0

let x0 be Real; :: thesis: ( x0 in X implies g /. x0 = (x0 * r0) + p0 )
assume A2: x0 in X ; :: thesis: g /. x0 = (x0 * r0) + p0
A3: x0 * r = x0 * r0 by REAL_NS1:3;
thus g /. x0 = f /. x0 by REAL_NS1:def 4
.= (x0 * r) + p by A2, A1
.= (x0 * r0) + p0 by A3, REAL_NS1:2 ; :: thesis: verum

end;

then g | X is continuous by NFCONT_3:33;
hence f | X is continuous by Th23; :: thesis: verum