let X be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S
for r, p being Point of S st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S
for r, p being Point of S st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let f be PartFunc of REAL, the carrier of S; :: thesis: for r, p being Point of S st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let r, p be Point of S; :: thesis: ( ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) implies f | X is continuous )
assume A1: for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ; :: thesis: f | X is continuous

A2: now

let x1, x2 be real number ; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * (abs (x1 - x2)) )
assume A3: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * (abs (x1 - x2))
then x2 in X by RELAT_1:86;
then A5: f /. x2 = (x2 * r) + p by A1;
A6: 0 <= abs (x1 - x2) by COMPLEX1:132;
X1: x1 - x2 is Real by XREAL_0:def 1;
x1 in X by A3, RELAT_1:86;
then f /. x1 = (x1 * r) + p by A1;
then ||.((f /. x1) - (f /. x2)).|| = ||.((x1 * r) + (p - (p + (x2 * r)))).|| by A5, RLVECT_1:def 6
.= ||.((x1 * r) + ((p - p) - (x2 * r))).|| by RLVECT_1:41
.= ||.((x1 * r) + ((0. S) - (x2 * r))).|| by RLVECT_1:28
.= ||.((x1 * r) - (x2 * r)).|| by RLVECT_1:27
.= ||.((x1 - x2) * r).|| by RLVECT_1:49
.= (abs (x1 - x2)) * ||.r.|| by X1, NORMSP_1:def 2 ;
then ||.((f /. x1) - (f /. x2)).|| + 0 <= (||.r.|| * (abs (x1 - x2))) + (1 * (abs (x1 - x2))) by A6, XREAL_1:9;
hence ||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * (abs (x1 - x2)) ; :: thesis: verum

end;

0 + 0 < ||.r.|| + 1 by NORMSP_1:8, XREAL_1:10;
then f | X is Lipschitzian by A2, Th33;
hence f | X is continuous ; :: thesis: verum