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;

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

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

then
g | X is continuous
by NFCONT_3:33;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;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

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