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,() by REAL_NS1:def 4;
reconsider r0 = r, p0 = p as Point of () 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 ; :: thesis: verum
end;
then g | X is continuous by NFCONT_3:33;
hence f | X is continuous by Th23; :: thesis: verum