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 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 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 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 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

A2: now :: thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * |.(x1 - x2).|

let x1, x2 be Real; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * |.(x1 - x2).| )
assume A3: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * |.(x1 - x2).|
then x2 in X ;
then A4: f /. x2 = (x2 * r) + p by A1;
A5: 0 <= |.(x1 - x2).| by COMPLEX1:46;
x1 in X by A3;
then f /. x1 = (x1 * r) + p by A1;
then ||.((f /. x1) - (f /. x2)).|| = ||.((x1 * r) + (p - (p + (x2 * r)))).|| by A4, RLVECT_1:def 3
.= ||.((x1 * r) + ((p - p) - (x2 * r))).|| by RLVECT_1:27
.= ||.((x1 * r) + ((0. S) - (x2 * r))).|| by RLVECT_1:15
.= ||.((x1 * r) - (x2 * r)).|| by RLVECT_1:14
.= ||.((x1 - x2) * r).|| by RLVECT_1:35
.= |.(x1 - x2).| * ||.r.|| by NORMSP_1:def 1 ;
then ||.((f /. x1) - (f /. x2)).|| + 0 <= (||.r.|| * |.(x1 - x2).|) + (1 * |.(x1 - x2).|) by A5, XREAL_1:7;
hence ||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * |.(x1 - x2).| ; :: thesis: verum

end;

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