let CNS be ComplexNormSpace; :: thesis: for X being set
for f being PartFunc of CNS,CNS
for z being Complex
for p being Point of CNS st X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f /. x0 = (z * x0) + p ) holds
f is_continuous_on X
let X be set ; :: thesis: for f being PartFunc of CNS,CNS
for z being Complex
for p being Point of CNS st X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f /. x0 = (z * x0) + p ) holds
f is_continuous_on X
let f be PartFunc of CNS,CNS; :: thesis: for z being Complex
for p being Point of CNS st X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f /. x0 = (z * x0) + p ) holds
f is_continuous_on X
let z be Complex; :: thesis: for p being Point of CNS st X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f /. x0 = (z * x0) + p ) holds
f is_continuous_on X
let p be Point of CNS; :: thesis: ( X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f /. x0 = (z * x0) + p ) implies f is_continuous_on X )
assume that
A1: X c= dom f and
A2: for x0 being Point of CNS st x0 in X holds
f /. x0 = (z * x0) + p ; :: thesis: f is_continuous_on X

now :: thesis: ( 0 < |.z.| + 1 & ( for x1, x2 being Point of CNS st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= (|.z.| + 1) * ||.(x1 - x2).|| ) )

0 + 0 < |.z.| + 1 by COMPLEX1:46, XREAL_1:8;
hence 0 < |.z.| + 1 ; :: thesis: for x1, x2 being Point of CNS st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= (|.z.| + 1) * ||.(x1 - x2).||
let x1, x2 be Point of CNS; :: thesis: ( x1 in X & x2 in X implies ||.((f /. x1) - (f /. x2)).|| <= (|.z.| + 1) * ||.(x1 - x2).|| )
assume ( x1 in X & x2 in X ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= (|.z.| + 1) * ||.(x1 - x2).||
then ( f /. x1 = (z * x1) + p & f /. x2 = (z * x2) + p ) by A2;
then A3: ||.((f /. x1) - (f /. x2)).|| = ||.((z * x1) + (p - (p + (z * x2)))).|| by RLVECT_1:28
.= ||.((z * x1) + ((p - p) - (z * x2))).|| by RLVECT_1:27
.= ||.((z * x1) + ((0. CNS) - (z * x2))).|| by RLVECT_1:15
.= ||.((z * x1) + (- (z * x2))).|| by RLVECT_1:14
.= ||.((z * x1) - (z * x2)).|| by RLVECT_1:def 11
.= ||.(z * (x1 - x2)).|| by CLVECT_1:9
.= |.z.| * ||.(x1 - x2).|| by CLVECT_1:def 13 ;
0 <= ||.(x1 - x2).|| by CLVECT_1:105;
then ||.((f /. x1) - (f /. x2)).|| + 0 <= (|.z.| * ||.(x1 - x2).||) + (1 * ||.(x1 - x2).||) by A3, XREAL_1:7;
hence ||.((f /. x1) - (f /. x2)).|| <= (|.z.| + 1) * ||.(x1 - x2).|| ; :: thesis: verum

end;

then f is_Lipschitzian_on X by A1;
hence f is_continuous_on X by Th116; :: thesis: verum