:: NCFCONT2 semantic presentation

begin


definition
let X be set ;
let CNS1, CNS2 be ComplexNormSpace;
let f be PartFunc of CNS1,CNS2;
predf is_uniformly_continuous_on X means :Def1: :: NCFCONT2:def 1
( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) );
end;

:: deftheorem Def1 defines is_uniformly_continuous_on NCFCONT2:def_1_:_
 for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 holds
( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );

definition
let X be set ;
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let f be PartFunc of CNS,RNS;
predf is_uniformly_continuous_on X means :Def2: :: NCFCONT2:def 2
( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) );
end;

:: deftheorem Def2 defines is_uniformly_continuous_on NCFCONT2:def_2_:_
 for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS holds
( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );

definition
let X be set ;
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let f be PartFunc of RNS,CNS;
predf is_uniformly_continuous_on X means :Def3: :: NCFCONT2:def 3
( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) );
end;

:: deftheorem Def3 defines is_uniformly_continuous_on NCFCONT2:def_3_:_
 for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS holds
( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );

definition
let X be set ;
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,COMPLEX;
predf is_uniformly_continuous_on X means :Def4: :: NCFCONT2:def 4
( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) );
end;

:: deftheorem Def4 defines is_uniformly_continuous_on NCFCONT2:def_4_:_
 for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX holds
( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) ) );

definition
let X be set ;
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,REAL;
predf is_uniformly_continuous_on X means :Def5: :: NCFCONT2:def 5
( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((f /. x1) - (f /. x2)) < r ) ) ) );
end;

:: deftheorem Def5 defines is_uniformly_continuous_on NCFCONT2:def_5_:_
 for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL holds
( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((f /. x1) - (f /. x2)) < r ) ) ) ) );

definition
let X be set ;
let RNS be RealNormSpace;
let f be PartFunc of the carrier of RNS,COMPLEX;
predf is_uniformly_continuous_on X means :Def6: :: NCFCONT2:def 6
( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) );
end;

:: deftheorem Def6 defines is_uniformly_continuous_on NCFCONT2:def_6_:_
 for X being set
for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX holds
( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) ) );

theorem Th1: :: NCFCONT2:1
for X, X1 being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
proof
let X, X1 be set ; ::_thesis: for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
let CNS1, CNS2 be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
let f be PartFunc of CNS1,CNS2; ::_thesis: ( f is_uniformly_continuous_on X & X1 c= X implies f is_uniformly_continuous_on X1 )
assume that
A1: f is_uniformly_continuous_on X and
A2: X1 c= X ; ::_thesis: f is_uniformly_continuous_on X1
 X c= dom f by A1, Def1;
hence  X1 c= dom f by A2, XBOOLE_1:1; :: according to NCFCONT2:def_1 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, Def1;
take  s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
thus  0 < s by A3; ::_thesis: for x1, x2 being Point of CNS1 st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r
let x1, x2 be Point of CNS1; ::_thesis: ( x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s implies ||.((f /. x1) - (f /. x2)).|| < r )
assume  ( x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| < r
hence  ||.((f /. x1) - (f /. x2)).|| < r by A2, A4; ::_thesis: verum
end;

theorem Th2: :: NCFCONT2:2
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
proof
let X, X1 be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
let f be PartFunc of CNS,RNS; ::_thesis: ( f is_uniformly_continuous_on X & X1 c= X implies f is_uniformly_continuous_on X1 )
assume that
A1: f is_uniformly_continuous_on X and
A2: X1 c= X ; ::_thesis: f is_uniformly_continuous_on X1
 X c= dom f by A1, Def2;
hence  X1 c= dom f by A2, XBOOLE_1:1; :: according to NCFCONT2:def_2 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, Def2;
take  s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
thus  0 < s by A3; ::_thesis: for x1, x2 being Point of CNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r
let x1, x2 be Point of CNS; ::_thesis: ( x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s implies ||.((f /. x1) - (f /. x2)).|| < r )
assume  ( x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| < r
hence  ||.((f /. x1) - (f /. x2)).|| < r by A2, A4; ::_thesis: verum
end;

theorem Th3: :: NCFCONT2:3
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
proof
let X, X1 be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1
let f be PartFunc of RNS,CNS; ::_thesis: ( f is_uniformly_continuous_on X & X1 c= X implies f is_uniformly_continuous_on X1 )
assume that
A1: f is_uniformly_continuous_on X and
A2: X1 c= X ; ::_thesis: f is_uniformly_continuous_on X1
 X c= dom f by A1, Def3;
hence  X1 c= dom f by A2, XBOOLE_1:1; :: according to NCFCONT2:def_3 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, Def3;
take  s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of RNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
thus  0 < s by A3; ::_thesis: for x1, x2 being Point of RNS st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r
let x1, x2 be Point of RNS; ::_thesis: ( x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s implies ||.((f /. x1) - (f /. x2)).|| < r )
assume  ( x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| < r
hence  ||.((f /. x1) - (f /. x2)).|| < r by A2, A4; ::_thesis: verum
end;

theorem :: NCFCONT2:4
for X, X1 being set
for CNS1, CNS2 being ComplexNormSpace
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
proof
let X, X1 be set ; ::_thesis: for CNS1, CNS2 being ComplexNormSpace
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
let CNS1, CNS2 be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
let f1, f2 be PartFunc of CNS1,CNS2; ::_thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 + f2 is_uniformly_continuous_on X /\ X1 )
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1 ; ::_thesis: f1 + f2 is_uniformly_continuous_on X /\ X1
A3: f2 is_uniformly_continuous_on X /\ X1 by A2, Th1, XBOOLE_1:17;
then A4: X /\ X1 c= dom f2 by Def1;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1, Th1, XBOOLE_1:17;
then  X /\ X1 c= dom f1 by Def1;
then  X /\ X1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:19;
hence A6: X /\ X1 c= dom (f1 + f2) by VFUNCT_1:def_1; :: according to NCFCONT2:def_1 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
then A7: 0 < r / 2 by XREAL_1:215;
then consider s being Real such that
A8: 0 < s and
A9: for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A5, Def1;
consider g being Real such that
A10: 0 < g and
A11: for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds
||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A3, A7, Def1;
take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
thus  0 < p by A8, A10, XXREAL_0:15; ::_thesis: for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r
let x1, x2 be Point of CNS1; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r )
assume that
A12: x1 in X /\ X1 and
A13: x2 in X /\ X1 and
A14: ||.(x1 - x2).|| < p ; ::_thesis: ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r
 p <= g by XXREAL_0:17;
then  ||.(x1 - x2).|| < g by A14, XXREAL_0:2;
then A15: ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A11, A12, A13;
 p <= s by XXREAL_0:17;
then  ||.(x1 - x2).|| < s by A14, XXREAL_0:2;
then  ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A9, A12, A13;
then A16: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A15, XREAL_1:8;
A17: ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by CLVECT_1:def_13;
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| = ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).|| by A6, A12, VFUNCT_1:def_1
.= ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).|| by A6, A13, VFUNCT_1:def_1
.= ||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).|| by RLVECT_1:def_3
.= ||.((f1 /. x1) + (((f2 /. x1) - (f1 /. x2)) - (f2 /. x2))).|| by RLVECT_1:27
.= ||.((f1 /. x1) + (((- (f1 /. x2)) + (f2 /. x1)) - (f2 /. x2))).||
.= ||.((f1 /. x1) + ((- (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def_3
.= ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:def_3 ;
hence  ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r by A16, A17, XXREAL_0:2; ::_thesis: verum
end;

theorem :: NCFCONT2:5
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
proof
let X, X1 be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
let CNS be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
let f1, f2 be PartFunc of CNS,RNS; ::_thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 + f2 is_uniformly_continuous_on X /\ X1 )
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1 ; ::_thesis: f1 + f2 is_uniformly_continuous_on X /\ X1
A3: f2 is_uniformly_continuous_on X /\ X1 by A2, Th2, XBOOLE_1:17;
then A4: X /\ X1 c= dom f2 by Def2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1, Th2, XBOOLE_1:17;
then  X /\ X1 c= dom f1 by Def2;
then  X /\ X1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:19;
hence A6: X /\ X1 c= dom (f1 + f2) by VFUNCT_1:def_1; :: according to NCFCONT2:def_2 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
then A7: 0 < r / 2 by XREAL_1:215;
then consider s being Real such that
A8: 0 < s and
A9: for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A5, Def2;
consider g being Real such that
A10: 0 < g and
A11: for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds
||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A3, A7, Def2;
take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
thus  0 < p by A8, A10, XXREAL_0:15; ::_thesis: for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r
let x1, x2 be Point of CNS; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r )
assume that
A12: x1 in X /\ X1 and
A13: x2 in X /\ X1 and
A14: ||.(x1 - x2).|| < p ; ::_thesis: ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r
 p <= g by XXREAL_0:17;
then  ||.(x1 - x2).|| < g by A14, XXREAL_0:2;
then A15: ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A11, A12, A13;
 p <= s by XXREAL_0:17;
then  ||.(x1 - x2).|| < s by A14, XXREAL_0:2;
then  ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A9, A12, A13;
then A16: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A15, XREAL_1:8;
A17: ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:def_1;
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| = ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).|| by A6, A12, VFUNCT_1:def_1
.= ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).|| by A6, A13, VFUNCT_1:def_1
.= ||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).|| by RLVECT_1:def_3
.= ||.((f1 /. x1) + (((f2 /. x1) - (f1 /. x2)) - (f2 /. x2))).|| by RLVECT_1:27
.= ||.((f1 /. x1) + (((- (f1 /. x2)) + (f2 /. x1)) - (f2 /. x2))).||
.= ||.((f1 /. x1) + ((- (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def_3
.= ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:def_3 ;
hence  ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r by A16, A17, XXREAL_0:2; ::_thesis: verum
end;

theorem :: NCFCONT2:6
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
proof
let X, X1 be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
let CNS be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
let f1, f2 be PartFunc of RNS,CNS; ::_thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 + f2 is_uniformly_continuous_on X /\ X1 )
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1 ; ::_thesis: f1 + f2 is_uniformly_continuous_on X /\ X1
A3: f2 is_uniformly_continuous_on X /\ X1 by A2, Th3, XBOOLE_1:17;
then A4: X /\ X1 c= dom f2 by Def3;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1, Th3, XBOOLE_1:17;
then  X /\ X1 c= dom f1 by Def3;
then  X /\ X1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:19;
hence A6: X /\ X1 c= dom (f1 + f2) by VFUNCT_1:def_1; :: according to NCFCONT2:def_3 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
then A7: 0 < r / 2 by XREAL_1:215;
then consider s being Real such that
A8: 0 < s and
A9: for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A5, Def3;
consider g being Real such that
A10: 0 < g and
A11: for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds
||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A3, A7, Def3;
take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) )
thus  0 < p by A8, A10, XXREAL_0:15; ::_thesis: for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r
let x1, x2 be Point of RNS; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r )
assume that
A12: x1 in X /\ X1 and
A13: x2 in X /\ X1 and
A14: ||.(x1 - x2).|| < p ; ::_thesis: ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r
 p <= g by XXREAL_0:17;
then  ||.(x1 - x2).|| < g by A14, XXREAL_0:2;
then A15: ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A11, A12, A13;
 p <= s by XXREAL_0:17;
then  ||.(x1 - x2).|| < s by A14, XXREAL_0:2;
then  ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A9, A12, A13;
then A16: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A15, XREAL_1:8;
A17: ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by CLVECT_1:def_13;
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| = ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).|| by A6, A12, VFUNCT_1:def_1
.= ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).|| by A6, A13, VFUNCT_1:def_1
.= ||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).|| by RLVECT_1:def_3
.= ||.((f1 /. x1) + (((f2 /. x1) - (f1 /. x2)) - (f2 /. x2))).|| by RLVECT_1:27
.= ||.((f1 /. x1) + (((- (f1 /. x2)) + (f2 /. x1)) - (f2 /. x2))).||
.= ||.((f1 /. x1) + ((- (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def_3
.= ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:def_3 ;
hence  ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r by A16, A17, XXREAL_0:2; ::_thesis: verum
end;

theorem :: NCFCONT2:7
for X, X1 being set
for CNS1, CNS2 being ComplexNormSpace
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
proof
let X, X1 be set ; ::_thesis: for CNS1, CNS2 being ComplexNormSpace
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let CNS1, CNS2 be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let f1, f2 be PartFunc of CNS1,CNS2; ::_thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 - f2 is_uniformly_continuous_on X /\ X1 )
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1 ; ::_thesis: f1 - f2 is_uniformly_continuous_on X /\ X1
A3: f2 is_uniformly_continuous_on X /\ X1 by A2, Th1, XBOOLE_1:17;
then A4: X /\ X1 c= dom f2 by Def1;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1, Th1, XBOOLE_1:17;
then  X /\ X1 c= dom f1 by Def1;
then  X /\ X1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:19;
hence A6: X /\ X1 c= dom (f1 - f2) by VFUNCT_1:def_2; :: according to NCFCONT2:def_1 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
then A7: 0 < r / 2 by XREAL_1:215;
then consider s being Real such that
A8: 0 < s and
A9: for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A5, Def1;
consider g being Real such that
A10: 0 < g and
A11: for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds
||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A3, A7, Def1;
take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
thus  0 < p by A8, A10, XXREAL_0:15; ::_thesis: for x1, x2 being Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
let x1, x2 be Point of CNS1; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r )
assume that
A12: x1 in X /\ X1 and
A13: x2 in X /\ X1 and
A14: ||.(x1 - x2).|| < p ; ::_thesis: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
 p <= g by XXREAL_0:17;
then  ||.(x1 - x2).|| < g by A14, XXREAL_0:2;
then A15: ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A11, A12, A13;
 p <= s by XXREAL_0:17;
then  ||.(x1 - x2).|| < s by A14, XXREAL_0:2;
then  ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A9, A12, A13;
then A16: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A15, XREAL_1:8;
A17: ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by CLVECT_1:104;
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A6, A12, VFUNCT_1:def_2
.= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A6, A13, VFUNCT_1:def_2
.= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1:27
.= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:def_3
.= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def_3
.= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:27 ;
hence  ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r by A16, A17, XXREAL_0:2; ::_thesis: verum
end;

theorem :: NCFCONT2:8
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
proof
let X, X1 be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let CNS be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let f1, f2 be PartFunc of CNS,RNS; ::_thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 - f2 is_uniformly_continuous_on X /\ X1 )
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1 ; ::_thesis: f1 - f2 is_uniformly_continuous_on X /\ X1
A3: f2 is_uniformly_continuous_on X /\ X1 by A2, Th2, XBOOLE_1:17;
then A4: X /\ X1 c= dom f2 by Def2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1, Th2, XBOOLE_1:17;
then  X /\ X1 c= dom f1 by Def2;
then  X /\ X1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:19;
hence A6: X /\ X1 c= dom (f1 - f2) by VFUNCT_1:def_2; :: according to NCFCONT2:def_2 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
then A7: 0 < r / 2 by XREAL_1:215;
then consider s being Real such that
A8: 0 < s and
A9: for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A5, Def2;
consider g being Real such that
A10: 0 < g and
A11: for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds
||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A3, A7, Def2;
take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
thus  0 < p by A8, A10, XXREAL_0:15; ::_thesis: for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
let x1, x2 be Point of CNS; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r )
assume that
A12: x1 in X /\ X1 and
A13: x2 in X /\ X1 and
A14: ||.(x1 - x2).|| < p ; ::_thesis: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
 p <= g by XXREAL_0:17;
then  ||.(x1 - x2).|| < g by A14, XXREAL_0:2;
then A15: ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A11, A12, A13;
 p <= s by XXREAL_0:17;
then  ||.(x1 - x2).|| < s by A14, XXREAL_0:2;
then  ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A9, A12, A13;
then A16: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A15, XREAL_1:8;
A17: ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:3;
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A6, A12, VFUNCT_1:def_2
.= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A6, A13, VFUNCT_1:def_2
.= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1:27
.= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:def_3
.= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def_3
.= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:27 ;
hence  ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r by A16, A17, XXREAL_0:2; ::_thesis: verum
end;

theorem :: NCFCONT2:9
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
proof
let X, X1 be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let CNS be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
let f1, f2 be PartFunc of RNS,CNS; ::_thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 - f2 is_uniformly_continuous_on X /\ X1 )
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1 ; ::_thesis: f1 - f2 is_uniformly_continuous_on X /\ X1
A3: f2 is_uniformly_continuous_on X /\ X1 by A2, Th3, XBOOLE_1:17;
then A4: X /\ X1 c= dom f2 by Def3;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1, Th3, XBOOLE_1:17;
then  X /\ X1 c= dom f1 by Def3;
then  X /\ X1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:19;
hence A6: X /\ X1 c= dom (f1 - f2) by VFUNCT_1:def_2; :: according to NCFCONT2:def_3 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
then A7: 0 < r / 2 by XREAL_1:215;
then consider s being Real such that
A8: 0 < s and
A9: for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds
||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A5, Def3;
consider g being Real such that
A10: 0 < g and
A11: for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds
||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A3, A7, Def3;
take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) )
thus  0 < p by A8, A10, XXREAL_0:15; ::_thesis: for x1, x2 being Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
let x1, x2 be Point of RNS; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r )
assume that
A12: x1 in X /\ X1 and
A13: x2 in X /\ X1 and
A14: ||.(x1 - x2).|| < p ; ::_thesis: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r
 p <= g by XXREAL_0:17;
then  ||.(x1 - x2).|| < g by A14, XXREAL_0:2;
then A15: ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A11, A12, A13;
 p <= s by XXREAL_0:17;
then  ||.(x1 - x2).|| < s by A14, XXREAL_0:2;
then  ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A9, A12, A13;
then A16: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A15, XREAL_1:8;
A17: ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by CLVECT_1:104;
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A6, A12, VFUNCT_1:def_2
.= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A6, A13, VFUNCT_1:def_2
.= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1:27
.= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:def_3
.= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def_3
.= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:27 ;
hence  ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r by A16, A17, XXREAL_0:2; ::_thesis: verum
end;

theorem Th10: :: NCFCONT2:10
for X being set
for z being Complex
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for z being Complex
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
let z be Complex; ::_thesis: for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
let CNS1, CNS2 be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
let f be PartFunc of CNS1,CNS2; ::_thesis: ( f is_uniformly_continuous_on X implies z (#) f is_uniformly_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: z (#) f is_uniformly_continuous_on X
then  X c= dom f by Def1;
hence A2: X c= dom (z (#) f) by VFUNCT_2:def_2; :: according to NCFCONT2:def_1 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1,_x2_being_Point_of_CNS1_st_x1_in_X_&_x2_in_X_&_||.(x1_-_x2).||_<_s_holds_
||.(((z_(#)_f)_/._x1)_-_((z_(#)_f)_/._x2)).||_<_r_)_)
percases ( z = 0 or z <> 0 ) ;
supposeA3: z = 0 ; ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) ) )
assume A4: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
then consider s being Real such that
A5: 0 < s and
 for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, Def1;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
thus  0 < s by A5; ::_thesis: for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r
let x1, x2 be Point of CNS1; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r )
assume that
A6: x1 in X and
A7: x2 in X and
 ||.(x1 - x2).|| < s ; ::_thesis: ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| = ||.((z * (f /. x1)) - ((z (#) f) /. x2)).|| by A2, A6, VFUNCT_2:def_2
.= ||.((0. CNS2) - ((z (#) f) /. x2)).|| by A3, CLVECT_1:1
.= ||.((0. CNS2) - (z * (f /. x2))).|| by A2, A7, VFUNCT_2:def_2
.= ||.((0. CNS2) - (0. CNS2)).|| by A3, CLVECT_1:1
.= ||.(0. CNS2).|| by RLVECT_1:13
.= 0 by NORMSP_0:def_6 ;
hence  ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r by A4; ::_thesis: verum
end;
supposeA8: z <> 0 ; ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) ) )
A9: 0 < |.z.| by A8, COMPLEX1:47;
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
then  0 < r / |.z.| by A9, XREAL_1:139;
then consider s being Real such that
A10: 0 < s and
A11: for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r / |.z.| by A1, Def1;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
thus  0 < s by A10; ::_thesis: for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r
let x1, x2 be Point of CNS1; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r )
assume that
A12: x1 in X and
A13: x2 in X and
A14: ||.(x1 - x2).|| < s ; ::_thesis: ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r
A15: ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| = ||.((z * (f /. x1)) - ((z (#) f) /. x2)).|| by A2, A12, VFUNCT_2:def_2
.= ||.((z * (f /. x1)) - (z * (f /. x2))).|| by A2, A13, VFUNCT_2:def_2
.= ||.(z * ((f /. x1) - (f /. x2))).|| by CLVECT_1:9
.= |.z.| * ||.((f /. x1) - (f /. x2)).|| by CLVECT_1:def_13 ;
 |.z.| * ||.((f /. x1) - (f /. x2)).|| < (r / |.z.|) * |.z.| by A9, A11, A12, A13, A14, XREAL_1:68;
hence  ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r by A9, A15, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
hence  for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) ) ; ::_thesis: verum
end;

theorem Th11: :: NCFCONT2:11
for X being set
for r being Real
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
r (#) f is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for r being Real
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
r (#) f is_uniformly_continuous_on X
let r be Real; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
r (#) f is_uniformly_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
r (#) f is_uniformly_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
r (#) f is_uniformly_continuous_on X
let f be PartFunc of CNS,RNS; ::_thesis: ( f is_uniformly_continuous_on X implies r (#) f is_uniformly_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: r (#) f is_uniformly_continuous_on X
then  X c= dom f by Def2;
hence A2: X c= dom (r (#) f) by VFUNCT_1:def_4; :: according to NCFCONT2:def_2 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < r ) )
now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1,_x2_being_Point_of_CNS_st_x1_in_X_&_x2_in_X_&_||.(x1_-_x2).||_<_s_holds_
||.(((r_(#)_f)_/._x1)_-_((r_(#)_f)_/._x2)).||_<_p_)_)
percases ( r = 0 or r <> 0 ) ;
supposeA3: r = 0 ; ::_thesis: for p being Real st 0 < p holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p ) )
let p be Real; ::_thesis: ( 0 < p implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p ) ) )
assume A4: 0 < p ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p ) )
then consider s being Real such that
A5: 0 < s and
 for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p by A1, Def2;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p ) )
thus  0 < s by A5; ::_thesis: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p
let x1, x2 be Point of CNS; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p )
assume that
A6: x1 in X and
A7: x2 in X and
 ||.(x1 - x2).|| < s ; ::_thesis: ||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| = ||.((r * (f /. x1)) - ((r (#) f) /. x2)).|| by A2, A6, VFUNCT_1:def_4
.= ||.((0. RNS) - ((r (#) f) /. x2)).|| by A3, RLVECT_1:10
.= ||.((0. RNS) - (r * (f /. x2))).|| by A2, A7, VFUNCT_1:def_4
.= ||.((0. RNS) - (0. RNS)).|| by A3, RLVECT_1:10
.= ||.(0. RNS).|| by RLVECT_1:13
.= 0 by NORMSP_0:def_6 ;
hence  ||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p by A4; ::_thesis: verum
end;
supposeA8: r <> 0 ; ::_thesis: for p being Real st 0 < p holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p ) )
let p be Real; ::_thesis: ( 0 < p implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p ) ) )
A9: 0 < abs r by A8, COMPLEX1:47;
assume  0 < p ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p ) )
then  0 < p / (abs r) by A9, XREAL_1:139;
then consider s being Real such that
A10: 0 < s and
A11: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p / (abs r) by A1, Def2;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p ) )
thus  0 < s by A10; ::_thesis: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p
let x1, x2 be Point of CNS; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p )
assume that
A12: x1 in X and
A13: x2 in X and
A14: ||.(x1 - x2).|| < s ; ::_thesis: ||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p
A15: ||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| = ||.((r * (f /. x1)) - ((r (#) f) /. x2)).|| by A2, A12, VFUNCT_1:def_4
.= ||.((r * (f /. x1)) - (r * (f /. x2))).|| by A2, A13, VFUNCT_1:def_4
.= ||.(r * ((f /. x1) - (f /. x2))).|| by RLVECT_1:34
.= (abs r) * ||.((f /. x1) - (f /. x2)).|| by NORMSP_1:def_1 ;
 (abs r) * ||.((f /. x1) - (f /. x2)).|| < (p / (abs r)) * (abs r) by A9, A11, A12, A13, A14, XREAL_1:68;
hence  ||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < p by A9, A15, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
hence  for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| < r ) ) ; ::_thesis: verum
end;

theorem Th12: :: NCFCONT2:12
for X being set
for z being Complex
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for z being Complex
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
let z be Complex; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
let f be PartFunc of RNS,CNS; ::_thesis: ( f is_uniformly_continuous_on X implies z (#) f is_uniformly_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: z (#) f is_uniformly_continuous_on X
then  X c= dom f by Def3;
hence A2: X c= dom (z (#) f) by VFUNCT_2:def_2; :: according to NCFCONT2:def_3 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1,_x2_being_Point_of_RNS_st_x1_in_X_&_x2_in_X_&_||.(x1_-_x2).||_<_s_holds_
||.(((z_(#)_f)_/._x1)_-_((z_(#)_f)_/._x2)).||_<_r_)_)
percases ( z = 0 or z <> 0 ) ;
supposeA3: z = 0 ; ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) ) )
assume A4: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
then consider s being Real such that
A5: 0 < s and
 for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, Def3;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
thus  0 < s by A5; ::_thesis: for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r
let x1, x2 be Point of RNS; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r )
assume that
A6: x1 in X and
A7: x2 in X and
 ||.(x1 - x2).|| < s ; ::_thesis: ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| = ||.((z * (f /. x1)) - ((z (#) f) /. x2)).|| by A2, A6, VFUNCT_2:def_2
.= ||.((0. CNS) - ((z (#) f) /. x2)).|| by A3, CLVECT_1:1
.= ||.((0. CNS) - (z * (f /. x2))).|| by A2, A7, VFUNCT_2:def_2
.= ||.((0. CNS) - (0. CNS)).|| by A3, CLVECT_1:1
.= ||.(0. CNS).|| by RLVECT_1:13
.= 0 by NORMSP_0:def_6 ;
hence  ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r by A4; ::_thesis: verum
end;
supposeA8: z <> 0 ; ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) ) )
A9: 0 < |.z.| by A8, COMPLEX1:47;
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
then  0 < r / |.z.| by A9, XREAL_1:139;
then consider s being Real such that
A10: 0 < s and
A11: for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r / |.z.| by A1, Def3;
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) )
thus  0 < s by A10; ::_thesis: for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r
let x1, x2 be Point of RNS; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r )
assume that
A12: x1 in X and
A13: x2 in X and
A14: ||.(x1 - x2).|| < s ; ::_thesis: ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r
A15: ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| = ||.((z * (f /. x1)) - ((z (#) f) /. x2)).|| by A2, A12, VFUNCT_2:def_2
.= ||.((z * (f /. x1)) - (z * (f /. x2))).|| by A2, A13, VFUNCT_2:def_2
.= ||.(z * ((f /. x1) - (f /. x2))).|| by CLVECT_1:9
.= |.z.| * ||.((f /. x1) - (f /. x2)).|| by CLVECT_1:def_13 ;
 |.z.| * ||.((f /. x1) - (f /. x2)).|| < (r / |.z.|) * |.z.| by A9, A11, A12, A13, A14, XREAL_1:68;
hence  ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r by A9, A15, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
hence  for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| < r ) ) ; ::_thesis: verum
end;

theorem :: NCFCONT2:13
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let CNS1, CNS2 be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let f be PartFunc of CNS1,CNS2; ::_thesis: ( f is_uniformly_continuous_on X implies - f is_uniformly_continuous_on X )
A1: - f = (- 1r) (#) f by VFUNCT_2:23;
assume  f is_uniformly_continuous_on X ; ::_thesis: - f is_uniformly_continuous_on X
hence  - f is_uniformly_continuous_on X by A1, Th10; ::_thesis: verum
end;

theorem :: NCFCONT2:14
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let f be PartFunc of CNS,RNS; ::_thesis: ( f is_uniformly_continuous_on X implies - f is_uniformly_continuous_on X )
A1: - f = (- 1) (#) f by VFUNCT_1:23;
assume  f is_uniformly_continuous_on X ; ::_thesis: - f is_uniformly_continuous_on X
hence  - f is_uniformly_continuous_on X by A1, Th11; ::_thesis: verum
end;

theorem :: NCFCONT2:15
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
let f be PartFunc of RNS,CNS; ::_thesis: ( f is_uniformly_continuous_on X implies - f is_uniformly_continuous_on X )
A1: - f = (- 1r) (#) f by VFUNCT_2:23;
assume  f is_uniformly_continuous_on X ; ::_thesis: - f is_uniformly_continuous_on X
hence  - f is_uniformly_continuous_on X by A1, Th12; ::_thesis: verum
end;

theorem :: NCFCONT2:16
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
let CNS1, CNS2 be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
let f be PartFunc of CNS1,CNS2; ::_thesis: ( f is_uniformly_continuous_on X implies ||.f.|| is_uniformly_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: ||.f.|| is_uniformly_continuous_on X
then  X c= dom f by Def1;
hence A2: X c= dom ||.f.|| by NORMSP_0:def_3; :: according to NCFCONT2:def_5 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, Def1;
take  s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) )
thus  0 < s by A3; ::_thesis: for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r
let x1, x2 be Point of CNS1; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r )
assume that
A5: x1 in X and
A6: x2 in X and
A7: ||.(x1 - x2).|| < s ; ::_thesis: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) = abs ((||.f.|| . x1) - (||.f.|| /. x2)) by A2, A5, PARTFUN1:def_6
.= abs ((||.f.|| . x1) - (||.f.|| . x2)) by A2, A6, PARTFUN1:def_6
.= abs (||.(f /. x1).|| - (||.f.|| . x2)) by A2, A5, NORMSP_0:def_3
.= abs (||.(f /. x1).|| - ||.(f /. x2).||) by A2, A6, NORMSP_0:def_3 ;
then A8: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= ||.((f /. x1) - (f /. x2)).|| by CLVECT_1:110;
 ||.((f /. x1) - (f /. x2)).|| < r by A4, A5, A6, A7;
hence  abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r by A8, XXREAL_0:2; ::_thesis: verum
end;

theorem :: NCFCONT2:17
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
let f be PartFunc of CNS,RNS; ::_thesis: ( f is_uniformly_continuous_on X implies ||.f.|| is_uniformly_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: ||.f.|| is_uniformly_continuous_on X
then  X c= dom f by Def2;
hence A2: X c= dom ||.f.|| by NORMSP_0:def_3; :: according to NCFCONT2:def_5 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) )
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, Def2;
take  s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) )
thus  0 < s by A3; ::_thesis: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r
let x1, x2 be Point of CNS; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r )
assume that
A5: x1 in X and
A6: x2 in X and
A7: ||.(x1 - x2).|| < s ; ::_thesis: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) = abs ((||.f.|| . x1) - (||.f.|| /. x2)) by A2, A5, PARTFUN1:def_6
.= abs ((||.f.|| . x1) - (||.f.|| . x2)) by A2, A6, PARTFUN1:def_6
.= abs (||.(f /. x1).|| - (||.f.|| . x2)) by A2, A5, NORMSP_0:def_3
.= abs (||.(f /. x1).|| - ||.(f /. x2).||) by A2, A6, NORMSP_0:def_3 ;
then A8: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= ||.((f /. x1) - (f /. x2)).|| by NORMSP_1:9;
 ||.((f /. x1) - (f /. x2)).|| < r by A4, A5, A6, A7;
hence  abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r by A8, XXREAL_0:2; ::_thesis: verum
end;

theorem :: NCFCONT2:18
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
let f be PartFunc of RNS,CNS; ::_thesis: ( f is_uniformly_continuous_on X implies ||.f.|| is_uniformly_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: ||.f.|| is_uniformly_continuous_on X
then  X c= dom f by Def3;
then A2: X c= dom ||.f.|| by NORMSP_0:def_3;
 for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) )
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, Def3;
take  s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) )
thus  0 < s by A3; ::_thesis: for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r
let x1, x2 be Point of RNS; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r )
assume that
A5: x1 in X and
A6: x2 in X and
A7: ||.(x1 - x2).|| < s ; ::_thesis: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r
abs ((||.f.|| /. x1) - (||.f.|| /. x2)) = abs ((||.f.|| . x1) - (||.f.|| /. x2)) by A2, A5, PARTFUN1:def_6
.= abs ((||.f.|| . x1) - (||.f.|| . x2)) by A2, A6, PARTFUN1:def_6
.= abs (||.(f /. x1).|| - (||.f.|| . x2)) by A2, A5, NORMSP_0:def_3
.= abs (||.(f /. x1).|| - ||.(f /. x2).||) by A2, A6, NORMSP_0:def_3 ;
then A8: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= ||.((f /. x1) - (f /. x2)).|| by CLVECT_1:110;
 ||.((f /. x1) - (f /. x2)).|| < r by A4, A5, A6, A7;
hence  abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r by A8, XXREAL_0:2; ::_thesis: verum
end;
hence  ||.f.|| is_uniformly_continuous_on X by A2, NFCONT_2:def_2; ::_thesis: verum
end;

theorem Th19: :: NCFCONT2:19
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
f is_continuous_on X
proof
let X be set ; ::_thesis: for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
f is_continuous_on X
let CNS1, CNS2 be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
f is_continuous_on X
let f be PartFunc of CNS1,CNS2; ::_thesis: ( f is_uniformly_continuous_on X implies f is_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: f is_continuous_on X
A2: now__::_thesis:_for_x0_being_Point_of_CNS1
for_r_being_Real_st_x0_in_X_&_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1_being_Point_of_CNS1_st_x1_in_X_&_||.(x1_-_x0).||_<_s_holds_
||.((f_/._x1)_-_(f_/._x0)).||_<_r_)_)
let x0 be Point of CNS1; ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
consider s being Real such that
A5: 0 < s and
A6: for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, A4, Def1;
take s = s; ::_thesis: ( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
thus  0 < s by A5; ::_thesis: for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r
let x1 be Point of CNS1; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.((f /. x1) - (f /. x0)).|| < r )
assume  ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < r
hence  ||.((f /. x1) - (f /. x0)).|| < r by A3, A6; ::_thesis: verum
end;
 X c= dom f by A1, Def1;
hence  f is_continuous_on X by A2, NCFCONT1:44; ::_thesis: verum
end;

theorem Th20: :: NCFCONT2:20
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
proof
let X be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
let f be PartFunc of CNS,RNS; ::_thesis: ( f is_uniformly_continuous_on X implies f is_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: f is_continuous_on X
A2: now__::_thesis:_for_x0_being_Point_of_CNS
for_r_being_Real_st_x0_in_X_&_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1_being_Point_of_CNS_st_x1_in_X_&_||.(x1_-_x0).||_<_s_holds_
||.((f_/._x1)_-_(f_/._x0)).||_<_r_)_)
let x0 be Point of CNS; ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
consider s being Real such that
A5: 0 < s and
A6: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, A4, Def2;
take s = s; ::_thesis: ( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
thus  0 < s by A5; ::_thesis: for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r
let x1 be Point of CNS; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.((f /. x1) - (f /. x0)).|| < r )
assume  ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < r
hence  ||.((f /. x1) - (f /. x0)).|| < r by A3, A6; ::_thesis: verum
end;
 X c= dom f by A1, Def2;
hence  f is_continuous_on X by A2, NCFCONT1:45; ::_thesis: verum
end;

theorem Th21: :: NCFCONT2:21
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
proof
let X be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
let f be PartFunc of RNS,CNS; ::_thesis: ( f is_uniformly_continuous_on X implies f is_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: f is_continuous_on X
A2: now__::_thesis:_for_x0_being_Point_of_RNS
for_r_being_Real_st_x0_in_X_&_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1_being_Point_of_RNS_st_x1_in_X_&_||.(x1_-_x0).||_<_s_holds_
||.((f_/._x1)_-_(f_/._x0)).||_<_r_)_)
let x0 be Point of RNS; ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
consider s being Real such that
A5: 0 < s and
A6: for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r by A1, A4, Def3;
take s = s; ::_thesis: ( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
thus  0 < s by A5; ::_thesis: for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r
let x1 be Point of RNS; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.((f /. x1) - (f /. x0)).|| < r )
assume  ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < r
hence  ||.((f /. x1) - (f /. x0)).|| < r by A3, A6; ::_thesis: verum
end;
 X c= dom f by A1, Def3;
hence  f is_continuous_on X by A2, NCFCONT1:46; ::_thesis: verum
end;

theorem :: NCFCONT2:22
for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX st f is_uniformly_continuous_on X holds
f is_continuous_on X
proof
let X be set ; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX st f is_uniformly_continuous_on X holds
f is_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of the carrier of CNS,COMPLEX st f is_uniformly_continuous_on X holds
f is_continuous_on X
let f be PartFunc of the carrier of CNS,COMPLEX; ::_thesis: ( f is_uniformly_continuous_on X implies f is_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: f is_continuous_on X
A2: now__::_thesis:_for_x0_being_Point_of_CNS
for_r_being_Real_st_x0_in_X_&_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1_being_Point_of_CNS_st_x1_in_X_&_||.(x1_-_x0).||_<_s_holds_
|.((f_/._x1)_-_(f_/._x0)).|_<_r_)_)
let x0 be Point of CNS; ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
consider s being Real such that
A5: 0 < s and
A6: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r by A1, A4, Def4;
take s = s; ::_thesis: ( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus  0 < s by A5; ::_thesis: for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be Point of CNS; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies |.((f /. x1) - (f /. x0)).| < r )
assume  ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r
hence  |.((f /. x1) - (f /. x0)).| < r by A3, A6; ::_thesis: verum
end;
 X c= dom f by A1, Def4;
hence  f is_continuous_on X by A2, NCFCONT1:47; ::_thesis: verum
end;

theorem Th23: :: NCFCONT2:23
for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL st f is_uniformly_continuous_on X holds
f is_continuous_on X
proof
let X be set ; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL st f is_uniformly_continuous_on X holds
f is_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of the carrier of CNS,REAL st f is_uniformly_continuous_on X holds
f is_continuous_on X
let f be PartFunc of the carrier of CNS,REAL; ::_thesis: ( f is_uniformly_continuous_on X implies f is_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: f is_continuous_on X
A2: now__::_thesis:_for_x0_being_Point_of_CNS
for_r_being_Real_st_x0_in_X_&_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1_being_Point_of_CNS_st_x1_in_X_&_||.(x1_-_x0).||_<_s_holds_
abs_((f_/._x1)_-_(f_/._x0))_<_r_)_)
let x0 be Point of CNS; ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
abs ((f /. x1) - (f /. x0)) < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
abs ((f /. x1) - (f /. x0)) < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
abs ((f /. x1) - (f /. x0)) < r ) )
consider s being Real such that
A5: 0 < s and
A6: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((f /. x1) - (f /. x2)) < r by A1, A4, Def5;
take s = s; ::_thesis: ( 0 < s & ( for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
abs ((f /. x1) - (f /. x0)) < r ) )
thus  0 < s by A5; ::_thesis: for x1 being Point of CNS st x1 in X & ||.(x1 - x0).|| < s holds
abs ((f /. x1) - (f /. x0)) < r
let x1 be Point of CNS; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies abs ((f /. x1) - (f /. x0)) < r )
assume  ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: abs ((f /. x1) - (f /. x0)) < r
hence  abs ((f /. x1) - (f /. x0)) < r by A3, A6; ::_thesis: verum
end;
 X c= dom f by A1, Def5;
hence  f is_continuous_on X by A2, NCFCONT1:48; ::_thesis: verum
end;

theorem :: NCFCONT2:24
for X being set
for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX st f is_uniformly_continuous_on X holds
f is_continuous_on X
proof
let X be set ; ::_thesis: for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX st f is_uniformly_continuous_on X holds
f is_continuous_on X
let RNS be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of RNS,COMPLEX st f is_uniformly_continuous_on X holds
f is_continuous_on X
let f be PartFunc of the carrier of RNS,COMPLEX; ::_thesis: ( f is_uniformly_continuous_on X implies f is_continuous_on X )
assume A1: f is_uniformly_continuous_on X ; ::_thesis: f is_continuous_on X
A2: now__::_thesis:_for_x0_being_Point_of_RNS
for_r_being_Real_st_x0_in_X_&_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1_being_Point_of_RNS_st_x1_in_X_&_||.(x1_-_x0).||_<_s_holds_
|.((f_/._x1)_-_(f_/._x0)).|_<_r_)_)
let x0 be Point of RNS; ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
consider s being Real such that
A5: 0 < s and
A6: for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r by A1, A4, Def6;
take s = s; ::_thesis: ( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus  0 < s by A5; ::_thesis: for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be Point of RNS; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies |.((f /. x1) - (f /. x0)).| < r )
assume  ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r
hence  |.((f /. x1) - (f /. x0)).| < r by A3, A6; ::_thesis: verum
end;
 X c= dom f by A1, Def6;
hence  f is_continuous_on X by A2, NCFCONT1:49; ::_thesis: verum
end;

theorem Th25: :: NCFCONT2:25
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let CNS1, CNS2 be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let f be PartFunc of CNS1,CNS2; ::_thesis: ( f is_Lipschitzian_on X implies f is_uniformly_continuous_on X )
assume A1: f is_Lipschitzian_on X ; ::_thesis: f is_uniformly_continuous_on X
hence  X c= dom f by NCFCONT1:def_17; :: according to NCFCONT2:def_1 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
consider r being Real such that
A2: 0 < r and
A3: for x1, x2 being Point of CNS1 st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| by A1, NCFCONT1:def_17;
let p be Real; ::_thesis: ( 0 < p implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) ) )
assume A4: 0 < p ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) )
take s = p / r; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) )
thus  0 < s by A2, A4, XREAL_1:139; ::_thesis: for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p
let x1, x2 be Point of CNS1; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.((f /. x1) - (f /. x2)).|| < p )
assume  ( x1 in X & x2 in X & ||.(x1 - x2).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| < p
then  ( r * ||.(x1 - x2).|| < s * r & ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) by A2, A3, XREAL_1:68;
then  ||.((f /. x1) - (f /. x2)).|| < (p / r) * r by XXREAL_0:2;
hence  ||.((f /. x1) - (f /. x2)).|| < p by A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem Th26: :: NCFCONT2:26
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let f be PartFunc of CNS,RNS; ::_thesis: ( f is_Lipschitzian_on X implies f is_uniformly_continuous_on X )
assume A1: f is_Lipschitzian_on X ; ::_thesis: f is_uniformly_continuous_on X
hence  X c= dom f by NCFCONT1:def_18; :: according to NCFCONT2:def_2 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
consider r being Real such that
A2: 0 < r and
A3: for x1, x2 being Point of CNS st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| by A1, NCFCONT1:def_18;
let p be Real; ::_thesis: ( 0 < p implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) ) )
assume A4: 0 < p ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) )
take s = p / r; ::_thesis: ( 0 < s & ( for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) )
thus  0 < s by A2, A4, XREAL_1:139; ::_thesis: for x1, x2 being Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p
let x1, x2 be Point of CNS; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.((f /. x1) - (f /. x2)).|| < p )
assume  ( x1 in X & x2 in X & ||.(x1 - x2).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| < p
then  ( r * ||.(x1 - x2).|| < s * r & ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) by A2, A3, XREAL_1:68;
then  ||.((f /. x1) - (f /. x2)).|| < (p / r) * r by XXREAL_0:2;
hence  ||.((f /. x1) - (f /. x2)).|| < p by A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem Th27: :: NCFCONT2:27
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
proof
let X be set ; ::_thesis: for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let f be PartFunc of RNS,CNS; ::_thesis: ( f is_Lipschitzian_on X implies f is_uniformly_continuous_on X )
assume A1: f is_Lipschitzian_on X ; ::_thesis: f is_uniformly_continuous_on X
hence  X c= dom f by NCFCONT1:def_19; :: according to NCFCONT2:def_3 ::_thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
consider r being Real such that
A2: 0 < r and
A3: for x1, x2 being Point of RNS st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| by A1, NCFCONT1:def_19;
let p be Real; ::_thesis: ( 0 < p implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) ) )
assume A4: 0 < p ; ::_thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) )
take s = p / r; ::_thesis: ( 0 < s & ( for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) )
thus  0 < s by A2, A4, XREAL_1:139; ::_thesis: for x1, x2 being Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p
let x1, x2 be Point of RNS; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.((f /. x1) - (f /. x2)).|| < p )
assume  ( x1 in X & x2 in X & ||.(x1 - x2).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| < p
then  ( r * ||.(x1 - x2).|| < s * r & ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) by A2, A3, XREAL_1:68;
then  ||.((f /. x1) - (f /. x2)).|| < (p / r) * r by XXREAL_0:2;
hence  ||.((f /. x1) - (f /. x2)).|| < p by A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: NCFCONT2:28
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for Y being Subset of CNS1 st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
proof
let CNS1, CNS2 be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS1,CNS2
for Y being Subset of CNS1 st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let f be PartFunc of CNS1,CNS2; ::_thesis: for Y being Subset of CNS1 st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let Y be Subset of CNS1; ::_thesis: ( Y is compact & f is_continuous_on Y implies f is_uniformly_continuous_on Y )
assume that
A1: Y is compact and
A2: f is_continuous_on Y ; ::_thesis: f is_uniformly_continuous_on Y
A3: Y c= dom f by A2, NCFCONT1:def_11;
assume  not f is_uniformly_continuous_on Y ; ::_thesis: contradiction
then consider r being Real such that
A4: 0 < r and
A5: for s being Real st 0 < s holds
ex x1, x2 being Point of CNS1 st
( x1 in Y & x2 in Y & ||.(x1 - x2).|| < s & not ||.((f /. x1) - (f /. x2)).|| < r ) by A3, Def1;
defpred S1[ Element of NAT , Point of CNS1] means ( $2 in Y & ex x2 being Point of CNS1 st
( x2 in Y & ||.($2 - x2).|| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x2)).|| < r ) );
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<_1_/_(n_+_1)
let n be Element of NAT ; ::_thesis: 0 < 1 / (n + 1)
 0 < n + 1 by NAT_1:5;
hence  0 < 1 / (n + 1) by XREAL_1:139; ::_thesis: verum
end;
A7: now__::_thesis:_for_n_being_Element_of_NAT_ex_x1_being_Point_of_CNS1_st_S1[n,x1]
let n be Element of NAT ; ::_thesis: ex x1 being Point of CNS1 st S1[n,x1]
consider x1 being Point of CNS1 such that
A8: ex x2 being Point of CNS1 st
( x1 in Y & x2 in Y & ||.(x1 - x2).|| < 1 / (n + 1) & not ||.((f /. x1) - (f /. x2)).|| < r ) by A5, A6;
take x1 = x1; ::_thesis: S1[n,x1]
thus  S1[n,x1] by A8; ::_thesis: verum
end;
consider s1 being sequence of CNS1 such that
A9: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A7);
defpred S2[ Element of NAT , Point of CNS1] means ( $2 in Y & ||.((s1 . $1) - $2).|| < 1 / ($1 + 1) & not ||.((f /. (s1 . $1)) - (f /. $2)).|| < r );
A10: for n being Element of NAT ex x2 being Point of CNS1 st S2[n,x2] by A9;
consider s2 being sequence of CNS1 such that
A11: for n being Element of NAT holds S2[n,s2 . n] from FUNCT_2:sch_3(A10);
now__::_thesis:_for_x_being_Point_of_CNS1_st_x_in_rng_s1_holds_
x_in_Y
let x be Point of CNS1; ::_thesis: ( x in rng s1 implies x in Y )
assume  x in rng s1 ; ::_thesis: x in Y
then  ex n being Element of NAT st x = s1 . n by NCFCONT1:7;
hence  x in Y by A9; ::_thesis: verum
end;
then  for x being set st x in rng s1 holds
x in Y ;
then A12: rng s1 c= Y by TARSKI:def_3;
then consider q1 being sequence of CNS1 such that
A13: q1 is subsequence of s1 and
A14: q1 is convergent and
A15: lim q1 in Y by A1, NCFCONT1:def_2;
consider Ns1 being V37() sequence of NAT such that
A16: q1 = s1 * Ns1 by A13, VALUED_0:def_17;
set q2 = q1 - ((s1 - s2) * Ns1);
A17: f | Y is_continuous_in lim q1 by A2, A15, NCFCONT1:def_11;
now__::_thesis:_for_x_being_set_st_x_in_rng_s2_holds_
x_in_Y
let x be set ; ::_thesis: ( x in rng s2 implies x in Y )
assume  x in rng s2 ; ::_thesis: x in Y
then  ex n being Element of NAT st x = s2 . n by NCFCONT1:7;
hence  x in Y by A11; ::_thesis: verum
end;
then A18: rng s2 c= Y by TARSKI:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(q1_-_((s1_-_s2)_*_Ns1))_._n_=_(s2_*_Ns1)_._n
let n be Element of NAT ; ::_thesis: (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n
thus (q1 - ((s1 - s2) * Ns1)) . n = ((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n) by A16, NORMSP_1:def_3
.= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:15
.= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:15
.= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by NORMSP_1:def_3
.= ((s1 . (Ns1 . n)) - (s1 . (Ns1 . n))) + (s2 . (Ns1 . n)) by RLVECT_1:29
.= (0. CNS1) + (s2 . (Ns1 . n)) by RLVECT_1:15
.= s2 . (Ns1 . n) by RLVECT_1:4
.= (s2 * Ns1) . n by FUNCT_2:15 ; ::_thesis: verum
end;
then A19: q1 - ((s1 - s2) * Ns1) = s2 * Ns1 by FUNCT_2:63;
then  rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21;
then A20: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A18, XBOOLE_1:1;
then  rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A3, XBOOLE_1:1;
then  rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A20, XBOOLE_1:19;
then A21: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61;
A22: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
||.(((s1_-_s2)_._m)_-_(0._CNS1)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((s1 - s2) . m) - (0. CNS1)).|| < p )
assume A23: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((s1 - s2) . m) - (0. CNS1)).|| < p
A24: 0 < p " by A23;
consider k being Element of NAT  such that
A25: p " < k by SEQ_4:3;
take k = k; ::_thesis: for m being Element of NAT st k <= m holds
||.(((s1 - s2) . m) - (0. CNS1)).|| < p
let m be Element of NAT ; ::_thesis: ( k <= m implies ||.(((s1 - s2) . m) - (0. CNS1)).|| < p )
assume  k <= m ; ::_thesis: ||.(((s1 - s2) . m) - (0. CNS1)).|| < p
then  k + 1 <= m + 1 by XREAL_1:6;
then  1 / (m + 1) <= 1 / (k + 1) by A25, A24, XREAL_1:118;
then A26: ||.((s1 . m) - (s2 . m)).|| < 1 / (k + 1) by A11, XXREAL_0:2;
 k < k + 1 by NAT_1:13;
then  p " < k + 1 by A25, XXREAL_0:2;
then  1 / (k + 1) < 1 / (p ") by A23, XREAL_1:76;
then A27: 1 / (k + 1) < p by XCMPLX_1:216;
||.(((s1 - s2) . m) - (0. CNS1)).|| = ||.(((s1 . m) - (s2 . m)) - (0. CNS1)).|| by NORMSP_1:def_3
.= ||.((s1 . m) - (s2 . m)).|| by RLVECT_1:13 ;
hence  ||.(((s1 - s2) . m) - (0. CNS1)).|| < p by A27, A26, XXREAL_0:2; ::_thesis: verum
end;
then A28: s1 - s2 is convergent by CLVECT_1:def_15;
then A29: (s1 - s2) * Ns1 is convergent by CLOPBAN3:7;
then A30: q1 - ((s1 - s2) * Ns1) is convergent by A14, CLVECT_1:114;
 rng q1 c= rng s1 by A13, VALUED_0:21;
then A31: rng q1 c= Y by A12, XBOOLE_1:1;
then  rng q1 c= dom f by A3, XBOOLE_1:1;
then  rng q1 c= (dom f) /\ Y by A31, XBOOLE_1:19;
then A32: rng q1 c= dom (f | Y) by RELAT_1:61;
then A33: (f | Y) /. (lim q1) = lim ((f | Y) /* q1) by A14, A17, NCFCONT1:def_5;
A34: (f | Y) /* q1 is convergent by A14, A17, A32, NCFCONT1:def_5;
 lim (s1 - s2) = 0. CNS1 by A22, A28, CLVECT_1:def_16;
then  lim ((s1 - s2) * Ns1) = 0. CNS1 by A28, CLOPBAN3:8;
then A35: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - (0. CNS1) by A14, A29, CLVECT_1:120
.= lim q1 by RLVECT_1:13 ;
then A36: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A17, A30, A21, NCFCONT1:def_5;
then A37: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A34, CLVECT_1:114;
 (f | Y) /. (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A17, A30, A35, A21, NCFCONT1:def_5;
then A38: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) /. (lim q1)) - ((f | Y) /. (lim q1)) by A34, A33, A36, CLVECT_1:120
.= 0. CNS2 by RLVECT_1:15 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_contradiction
let n be Element of NAT ; ::_thesis: contradiction
consider k being Element of NAT  such that
A39: for m being Element of NAT st k <= m holds
||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - (0. CNS2)).|| < r by A4, A37, A38, CLVECT_1:def_16;
A40: q1 . k in rng q1 by NCFCONT1:7;
A41: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by NCFCONT1:7;
||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - (0. CNS2)).|| = ||.((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k).|| by RLVECT_1:13
.= ||.((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by NORMSP_1:def_3
.= ||.(((f | Y) /. (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by A32, FUNCT_2:109
.= ||.(((f | Y) /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A21, FUNCT_2:109
.= ||.((f /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A32, A40, PARTFUN2:15
.= ||.((f /. (q1 . k)) - (f /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A21, A41, PARTFUN2:15
.= ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A16, A19, FUNCT_2:15
.= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2:15 ;
hence  contradiction by A11, A39; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;

theorem :: NCFCONT2:29
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS
for Y being Subset of CNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
proof
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS
for Y being Subset of CNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of CNS,RNS
for Y being Subset of CNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let f be PartFunc of CNS,RNS; ::_thesis: for Y being Subset of CNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let Y be Subset of CNS; ::_thesis: ( Y is compact & f is_continuous_on Y implies f is_uniformly_continuous_on Y )
assume that
A1: Y is compact and
A2: f is_continuous_on Y ; ::_thesis: f is_uniformly_continuous_on Y
A3: Y c= dom f by A2, NCFCONT1:def_12;
assume  not f is_uniformly_continuous_on Y ; ::_thesis: contradiction
then consider r being Real such that
A4: 0 < r and
A5: for s being Real st 0 < s holds
ex x1, x2 being Point of CNS st
( x1 in Y & x2 in Y & ||.(x1 - x2).|| < s & not ||.((f /. x1) - (f /. x2)).|| < r ) by A3, Def2;
defpred S1[ Element of NAT , Point of CNS] means ( $2 in Y & ex x2 being Point of CNS st
( x2 in Y & ||.($2 - x2).|| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x2)).|| < r ) );
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<_1_/_(n_+_1)
let n be Element of NAT ; ::_thesis: 0 < 1 / (n + 1)
 0 < n + 1 by NAT_1:5;
hence  0 < 1 / (n + 1) by XREAL_1:139; ::_thesis: verum
end;
A7: now__::_thesis:_for_n_being_Element_of_NAT_ex_x1_being_Point_of_CNS_st_S1[n,x1]
let n be Element of NAT ; ::_thesis: ex x1 being Point of CNS st S1[n,x1]
consider x1 being Point of CNS such that
A8: ex x2 being Point of CNS st
( x1 in Y & x2 in Y & ||.(x1 - x2).|| < 1 / (n + 1) & not ||.((f /. x1) - (f /. x2)).|| < r ) by A5, A6;
take x1 = x1; ::_thesis: S1[n,x1]
thus  S1[n,x1] by A8; ::_thesis: verum
end;
consider s1 being sequence of CNS such that
A9: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A7);
defpred S2[ Element of NAT , Point of CNS] means ( $2 in Y & ||.((s1 . $1) - $2).|| < 1 / ($1 + 1) & not ||.((f /. (s1 . $1)) - (f /. $2)).|| < r );
A10: for n being Element of NAT ex x2 being Point of CNS st S2[n,x2] by A9;
consider s2 being sequence of CNS such that
A11: for n being Element of NAT holds S2[n,s2 . n] from FUNCT_2:sch_3(A10);
now__::_thesis:_for_x_being_Point_of_CNS_st_x_in_rng_s1_holds_
x_in_Y
let x be Point of CNS; ::_thesis: ( x in rng s1 implies x in Y )
assume  x in rng s1 ; ::_thesis: x in Y
then  ex n being Element of NAT st x = s1 . n by NCFCONT1:7;
hence  x in Y by A9; ::_thesis: verum
end;
then  for x being set st x in rng s1 holds
x in Y ;
then A12: rng s1 c= Y by TARSKI:def_3;
then consider q1 being sequence of CNS such that
A13: q1 is subsequence of s1 and
A14: q1 is convergent and
A15: lim q1 in Y by A1, NCFCONT1:def_2;
consider Ns1 being V37() sequence of NAT such that
A16: q1 = s1 * Ns1 by A13, VALUED_0:def_17;
set q2 = q1 - ((s1 - s2) * Ns1);
A17: f | Y is_continuous_in lim q1 by A2, A15, NCFCONT1:def_12;
now__::_thesis:_for_x_being_set_st_x_in_rng_s2_holds_
x_in_Y
let x be set ; ::_thesis: ( x in rng s2 implies x in Y )
assume  x in rng s2 ; ::_thesis: x in Y
then  ex n being Element of NAT st x = s2 . n by NCFCONT1:7;
hence  x in Y by A11; ::_thesis: verum
end;
then A18: rng s2 c= Y by TARSKI:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(q1_-_((s1_-_s2)_*_Ns1))_._n_=_(s2_*_Ns1)_._n
let n be Element of NAT ; ::_thesis: (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n
thus (q1 - ((s1 - s2) * Ns1)) . n = ((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n) by A16, NORMSP_1:def_3
.= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:15
.= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:15
.= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by NORMSP_1:def_3
.= ((s1 . (Ns1 . n)) - (s1 . (Ns1 . n))) + (s2 . (Ns1 . n)) by RLVECT_1:29
.= (0. CNS) + (s2 . (Ns1 . n)) by RLVECT_1:15
.= s2 . (Ns1 . n) by RLVECT_1:4
.= (s2 * Ns1) . n by FUNCT_2:15 ; ::_thesis: verum
end;
then A19: q1 - ((s1 - s2) * Ns1) = s2 * Ns1 by FUNCT_2:63;
then  rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21;
then A20: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A18, XBOOLE_1:1;
then  rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A3, XBOOLE_1:1;
then  rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A20, XBOOLE_1:19;
then A21: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61;
A22: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
||.(((s1_-_s2)_._m)_-_(0._CNS)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((s1 - s2) . m) - (0. CNS)).|| < p )
assume A23: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((s1 - s2) . m) - (0. CNS)).|| < p
A24: 0 < p " by A23;
consider k being Element of NAT  such that
A25: p " < k by SEQ_4:3;
take k = k; ::_thesis: for m being Element of NAT st k <= m holds
||.(((s1 - s2) . m) - (0. CNS)).|| < p
let m be Element of NAT ; ::_thesis: ( k <= m implies ||.(((s1 - s2) . m) - (0. CNS)).|| < p )
assume  k <= m ; ::_thesis: ||.(((s1 - s2) . m) - (0. CNS)).|| < p
then  k + 1 <= m + 1 by XREAL_1:6;
then  1 / (m + 1) <= 1 / (k + 1) by A25, A24, XREAL_1:118;
then A26: ||.((s1 . m) - (s2 . m)).|| < 1 / (k + 1) by A11, XXREAL_0:2;
 k < k + 1 by NAT_1:13;
then  p " < k + 1 by A25, XXREAL_0:2;
then  1 / (k + 1) < 1 / (p ") by A23, XREAL_1:76;
then A27: 1 / (k + 1) < p by XCMPLX_1:216;
||.(((s1 - s2) . m) - (0. CNS)).|| = ||.(((s1 . m) - (s2 . m)) - (0. CNS)).|| by NORMSP_1:def_3
.= ||.((s1 . m) - (s2 . m)).|| by RLVECT_1:13 ;
hence  ||.(((s1 - s2) . m) - (0. CNS)).|| < p by A27, A26, XXREAL_0:2; ::_thesis: verum
end;
then A28: s1 - s2 is convergent by CLVECT_1:def_15;
then A29: (s1 - s2) * Ns1 is convergent by CLOPBAN3:7;
then A30: q1 - ((s1 - s2) * Ns1) is convergent by A14, CLVECT_1:114;
 rng q1 c= rng s1 by A13, VALUED_0:21;
then A31: rng q1 c= Y by A12, XBOOLE_1:1;
then  rng q1 c= dom f by A3, XBOOLE_1:1;
then  rng q1 c= (dom f) /\ Y by A31, XBOOLE_1:19;
then A32: rng q1 c= dom (f | Y) by RELAT_1:61;
then A33: (f | Y) /. (lim q1) = lim ((f | Y) /* q1) by A14, A17, NCFCONT1:def_6;
A34: (f | Y) /* q1 is convergent by A14, A17, A32, NCFCONT1:def_6;
 lim (s1 - s2) = 0. CNS by A22, A28, CLVECT_1:def_16;
then  lim ((s1 - s2) * Ns1) = 0. CNS by A28, CLOPBAN3:8;
then A35: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - (0. CNS) by A14, A29, CLVECT_1:120
.= lim q1 by RLVECT_1:13 ;
then A36: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A17, A30, A21, NCFCONT1:def_6;
then A37: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A34, NORMSP_1:20;
 (f | Y) /. (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A17, A30, A35, A21, NCFCONT1:def_6;
then A38: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) /. (lim q1)) - ((f | Y) /. (lim q1)) by A34, A33, A36, NORMSP_1:26
.= 0. RNS by RLVECT_1:15 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_contradiction
let n be Element of NAT ; ::_thesis: contradiction
consider k being Element of NAT  such that
A39: for m being Element of NAT st k <= m holds
||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - (0. RNS)).|| < r by A4, A37, A38, NORMSP_1:def_7;
A40: q1 . k in rng q1 by NCFCONT1:7;
A41: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by NCFCONT1:7;
||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - (0. RNS)).|| = ||.((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k).|| by RLVECT_1:13
.= ||.((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by NORMSP_1:def_3
.= ||.(((f | Y) /. (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by A32, FUNCT_2:109
.= ||.(((f | Y) /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A21, FUNCT_2:109
.= ||.((f /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A32, A40, PARTFUN2:15
.= ||.((f /. (q1 . k)) - (f /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A21, A41, PARTFUN2:15
.= ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A16, A19, FUNCT_2:15
.= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2:15 ;
hence  contradiction by A11, A39; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;

theorem :: NCFCONT2:30
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
proof
let RNS be RealNormSpace; ::_thesis: for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let CNS be ComplexNormSpace; ::_thesis: for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let f be PartFunc of RNS,CNS; ::_thesis: for Y being Subset of RNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let Y be Subset of RNS; ::_thesis: ( Y is compact & f is_continuous_on Y implies f is_uniformly_continuous_on Y )
assume that
A1: Y is compact and
A2: f is_continuous_on Y ; ::_thesis: f is_uniformly_continuous_on Y
A3: Y c= dom f by A2, NCFCONT1:def_13;
assume  not f is_uniformly_continuous_on Y ; ::_thesis: contradiction
then consider r being Real such that
A4: 0 < r and
A5: for s being Real st 0 < s holds
ex x1, x2 being Point of RNS st
( x1 in Y & x2 in Y & ||.(x1 - x2).|| < s & not ||.((f /. x1) - (f /. x2)).|| < r ) by A3, Def3;
defpred S1[ Element of NAT , Point of RNS] means ( $2 in Y & ex x2 being Point of RNS st
( x2 in Y & ||.($2 - x2).|| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x2)).|| < r ) );
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<_1_/_(n_+_1)
let n be Element of NAT ; ::_thesis: 0 < 1 / (n + 1)
 0 < n + 1 by NAT_1:5;
hence  0 < 1 / (n + 1) by XREAL_1:139; ::_thesis: verum
end;
A7: now__::_thesis:_for_n_being_Element_of_NAT_ex_x1_being_Point_of_RNS_st_S1[n,x1]
let n be Element of NAT ; ::_thesis: ex x1 being Point of RNS st S1[n,x1]
consider x1 being Point of RNS such that
A8: ex x2 being Point of RNS st
( x1 in Y & x2 in Y & ||.(x1 - x2).|| < 1 / (n + 1) & not ||.((f /. x1) - (f /. x2)).|| < r ) by A5, A6;
take x1 = x1; ::_thesis: S1[n,x1]
thus  S1[n,x1] by A8; ::_thesis: verum
end;
consider s1 being sequence of RNS such that
A9: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A7);
defpred S2[ Element of NAT , Point of RNS] means ( $2 in Y & ||.((s1 . $1) - $2).|| < 1 / ($1 + 1) & not ||.((f /. (s1 . $1)) - (f /. $2)).|| < r );
A10: for n being Element of NAT ex x2 being Point of RNS st S2[n,x2] by A9;
consider s2 being sequence of RNS such that
A11: for n being Element of NAT holds S2[n,s2 . n] from FUNCT_2:sch_3(A10);
now__::_thesis:_for_x_being_Point_of_RNS_st_x_in_rng_s1_holds_
x_in_Y
let x be Point of RNS; ::_thesis: ( x in rng s1 implies x in Y )
assume  x in rng s1 ; ::_thesis: x in Y
then  ex n being Element of NAT st x = s1 . n by NFCONT_1:6;
hence  x in Y by A9; ::_thesis: verum
end;
then  for x being set st x in rng s1 holds
x in Y ;
then A12: rng s1 c= Y by TARSKI:def_3;
then consider q1 being sequence of RNS such that
A13: q1 is subsequence of s1 and
A14: q1 is convergent and
A15: lim q1 in Y by A1, NFCONT_1:def_2;
consider Ns1 being V37() sequence of NAT such that
A16: q1 = s1 * Ns1 by A13, VALUED_0:def_17;
set q2 = q1 - ((s1 - s2) * Ns1);
A17: f | Y is_continuous_in lim q1 by A2, A15, NCFCONT1:def_13;
now__::_thesis:_for_x_being_set_st_x_in_rng_s2_holds_
x_in_Y
let x be set ; ::_thesis: ( x in rng s2 implies x in Y )
assume  x in rng s2 ; ::_thesis: x in Y
then  ex n being Element of NAT st x = s2 . n by NFCONT_1:6;
hence  x in Y by A11; ::_thesis: verum
end;
then A18: rng s2 c= Y by TARSKI:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(q1_-_((s1_-_s2)_*_Ns1))_._n_=_(s2_*_Ns1)_._n
let n be Element of NAT ; ::_thesis: (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n
thus (q1 - ((s1 - s2) * Ns1)) . n = ((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n) by A16, NORMSP_1:def_3
.= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:15
.= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:15
.= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by NORMSP_1:def_3
.= ((s1 . (Ns1 . n)) - (s1 . (Ns1 . n))) + (s2 . (Ns1 . n)) by RLVECT_1:29
.= (0. RNS) + (s2 . (Ns1 . n)) by RLVECT_1:15
.= s2 . (Ns1 . n) by RLVECT_1:4
.= (s2 * Ns1) . n by FUNCT_2:15 ; ::_thesis: verum
end;
then A19: q1 - ((s1 - s2) * Ns1) = s2 * Ns1 by FUNCT_2:63;
then  rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21;
then A20: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A18, XBOOLE_1:1;
then  rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A3, XBOOLE_1:1;
then  rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A20, XBOOLE_1:19;
then A21: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61;
A22: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
||.(((s1_-_s2)_._m)_-_(0._RNS)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((s1 - s2) . m) - (0. RNS)).|| < p )
assume A23: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((s1 - s2) . m) - (0. RNS)).|| < p
A24: 0 < p " by A23;
consider k being Element of NAT  such that
A25: p " < k by SEQ_4:3;
take k = k; ::_thesis: for m being Element of NAT st k <= m holds
||.(((s1 - s2) . m) - (0. RNS)).|| < p
let m be Element of NAT ; ::_thesis: ( k <= m implies ||.(((s1 - s2) . m) - (0. RNS)).|| < p )
assume  k <= m ; ::_thesis: ||.(((s1 - s2) . m) - (0. RNS)).|| < p
then  k + 1 <= m + 1 by XREAL_1:6;
then  1 / (m + 1) <= 1 / (k + 1) by A25, A24, XREAL_1:118;
then A26: ||.((s1 . m) - (s2 . m)).|| < 1 / (k + 1) by A11, XXREAL_0:2;
 k < k + 1 by NAT_1:13;
then  p " < k + 1 by A25, XXREAL_0:2;
then  1 / (k + 1) < 1 / (p ") by A23, XREAL_1:76;
then A27: 1 / (k + 1) < p by XCMPLX_1:216;
||.(((s1 - s2) . m) - (0. RNS)).|| = ||.(((s1 . m) - (s2 . m)) - (0. RNS)).|| by NORMSP_1:def_3
.= ||.((s1 . m) - (s2 . m)).|| by RLVECT_1:13 ;
hence  ||.(((s1 - s2) . m) - (0. RNS)).|| < p by A27, A26, XXREAL_0:2; ::_thesis: verum
end;
then A28: s1 - s2 is convergent by NORMSP_1:def_6;
then A29: (s1 - s2) * Ns1 is convergent by LOPBAN_3:7;
then A30: q1 - ((s1 - s2) * Ns1) is convergent by A14, NORMSP_1:20;
 rng q1 c= rng s1 by A13, VALUED_0:21;
then A31: rng q1 c= Y by A12, XBOOLE_1:1;
then  rng q1 c= dom f by A3, XBOOLE_1:1;
then  rng q1 c= (dom f) /\ Y by A31, XBOOLE_1:19;
then A32: rng q1 c= dom (f | Y) by RELAT_1:61;
then A33: (f | Y) /. (lim q1) = lim ((f | Y) /* q1) by A14, A17, NCFCONT1:def_7;
A34: (f | Y) /* q1 is convergent by A14, A17, A32, NCFCONT1:def_7;
 lim (s1 - s2) = 0. RNS by A22, A28, NORMSP_1:def_7;
then  lim ((s1 - s2) * Ns1) = 0. RNS by A28, LOPBAN_3:8;
then A35: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - (0. RNS) by A14, A29, NORMSP_1:26
.= lim q1 by RLVECT_1:13 ;
then A36: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A17, A30, A21, NCFCONT1:def_7;
then A37: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A34, CLVECT_1:114;
 (f | Y) /. (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A17, A30, A35, A21, NCFCONT1:def_7;
then A38: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) /. (lim q1)) - ((f | Y) /. (lim q1)) by A34, A33, A36, CLVECT_1:120
.= 0. CNS by RLVECT_1:15 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_contradiction
let n be Element of NAT ; ::_thesis: contradiction
consider k being Element of NAT  such that
A39: for m being Element of NAT st k <= m holds
||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - (0. CNS)).|| < r by A4, A37, A38, CLVECT_1:def_16;
A40: q1 . k in rng q1 by NFCONT_1:6;
A41: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by NFCONT_1:6;
||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - (0. CNS)).|| = ||.((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k).|| by RLVECT_1:13
.= ||.((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by NORMSP_1:def_3
.= ||.(((f | Y) /. (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by A32, FUNCT_2:109
.= ||.(((f | Y) /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A21, FUNCT_2:109
.= ||.((f /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A32, A40, PARTFUN2:15
.= ||.((f /. (q1 . k)) - (f /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A21, A41, PARTFUN2:15
.= ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A16, A19, FUNCT_2:15
.= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2:15 ;
hence  contradiction by A11, A39; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;

theorem :: NCFCONT2:31
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for Y being Subset of CNS1 st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
f .: Y is compact by Th19, NCFCONT1:83;

theorem :: NCFCONT2:32
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS
for Y being Subset of CNS st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
f .: Y is compact by Th20, NCFCONT1:84;

theorem :: NCFCONT2:33
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
f .: Y is compact by Th21, NCFCONT1:85;

theorem :: NCFCONT2:34
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL
for Y being Subset of CNS st Y <> {} & Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
ex x1, x2 being Point of CNS st
( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) by Th23, NCFCONT1:96;

theorem :: NCFCONT2:35
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st X c= dom f & f | X is constant holds
f is_uniformly_continuous_on X by Th25, NCFCONT1:112;

theorem :: NCFCONT2:36
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st X c= dom f & f | X is constant holds
f is_uniformly_continuous_on X by Th26, NCFCONT1:113;

theorem :: NCFCONT2:37
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st X c= dom f & f | X is constant holds
f is_uniformly_continuous_on X by Th27, NCFCONT1:114;

begin

definition
let M be non empty CNORMSTR ;
let f be Function of M,M;
attrf is contraction  means :Def7: :: NCFCONT2:def 7
 ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) );
end;

:: deftheorem Def7 defines contraction NCFCONT2:def_7_:_
 for M being non empty CNORMSTR
for f being Function of M,M holds
( f is contraction iff ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) ) );

registration
let M be ComplexBanachSpace;
cluster non empty Relation-like the carrier of M -defined the carrier of M -valued Function-like total quasi_total contraction for Element of K6(K7( the carrier of M, the carrier of M));
existence
 ex b1 being Function of M,M st b1 is contraction
proof
set x = the Point of M;
reconsider f = the carrier of M --> the Point of M as Function of the carrier of M, the carrier of M ;
take  f ; ::_thesis: f is contraction
take  1 / 2 ; :: according to NCFCONT2:def_7 ::_thesis: ( 0 < 1 / 2 & 1 / 2 < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= (1 / 2) * ||.(x - y).|| ) )
thus  ( 0 < 1 / 2 & 1 / 2 < 1 ) ; ::_thesis: for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= (1 / 2) * ||.(x - y).||
let z, y be Point of M; ::_thesis: ||.((f . z) - (f . y)).|| <= (1 / 2) * ||.(z - y).||
 ( f . z = the Point of M & f . y = the Point of M ) by FUNCOP_1:7;
then A1: ||.((f . z) - (f . y)).|| = 0 by CLVECT_1:107;
 ||.(z - y).|| >= 0 by CLVECT_1:105;
hence  ||.((f . z) - (f . y)).|| <= (1 / 2) * ||.(z - y).|| by A1; ::_thesis: verum
end;
end;

definition
let M be ComplexBanachSpace;
mode Contraction of M is contraction Function of M,M;
end;

theorem :: NCFCONT2:38
for X being ComplexNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y )
proof
let X be ComplexNormSpace; ::_thesis: for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y )
let x, y be Point of X; ::_thesis: ( ||.(x - y).|| > 0 iff x <> y )
 ( 0 < ||.(x - y).|| implies x - y <> 0. X ) by NORMSP_0:def_6;
hence  ( 0 < ||.(x - y).|| implies x <> y ) by RLVECT_1:15; ::_thesis: ( x <> y implies ||.(x - y).|| > 0 )
now__::_thesis:_(_x_<>_y_implies_0_<_||.(x_-_y).||_)
assume  x <> y ; ::_thesis: 0 < ||.(x - y).||
then  0 <> ||.(x - y).|| by CLVECT_1:112;
hence  0 < ||.(x - y).|| by CLVECT_1:105; ::_thesis: verum
end;
hence  ( x <> y implies ||.(x - y).|| > 0 ) ; ::_thesis: verum
end;

theorem :: NCFCONT2:39
for X being ComplexNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).||
proof
let X be ComplexNormSpace; ::_thesis: for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).||
let x, y be Point of X; ::_thesis: ||.(x - y).|| = ||.(y - x).||
thus ||.(x - y).|| = ||.(- (x - y)).|| by CLVECT_1:103
.= ||.(y - x).|| by RLVECT_1:33 ; ::_thesis: verum
end;

Lm1:  for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
proof
let X be ComplexNormSpace; ::_thesis: for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
let x, y, z be Point of X; ::_thesis: for e being Real st ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
let e be Real; ::_thesis: ( ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 implies ||.(x - y).|| < e )
assume  ( ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 ) ; ::_thesis: ||.(x - y).|| < e
then  ||.(x - z).|| + ||.(z - y).|| < (e / 2) + (e / 2) by XREAL_1:8;
then  ||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||) < (||.(x - z).|| + ||.(z - y).||) + e by CLVECT_1:111, XREAL_1:8;
then  (||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) < (e + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) by XREAL_1:8;
hence  ||.(x - y).|| < e ; ::_thesis: verum
end;

Lm2:  for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
proof
let X be ComplexNormSpace; ::_thesis: for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
let x, y, z be Point of X; ::_thesis: for e being Real st ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
let e be Real; ::_thesis: ( ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 implies ||.(x - y).|| < e )
assume that
A1: ||.(x - z).|| < e / 2 and
A2: ||.(y - z).|| < e / 2 ; ::_thesis: ||.(x - y).|| < e
 ||.(- (y - z)).|| < e / 2 by A2, CLVECT_1:103;
then  ||.(z - y).|| < e / 2 by RLVECT_1:33;
hence  ||.(x - y).|| < e by A1, Lm1; ::_thesis: verum
end;

Lm3:  for X being ComplexNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
proof
let X be ComplexNormSpace; ::_thesis: for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
let x be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds
||.x.|| < e ) implies x = 0. X )
assume A1: for e being Real st e > 0 holds
||.x.|| < e ; ::_thesis: x = 0. X
now__::_thesis:_not_x_<>_0._X
assume  x <> 0. X ; ::_thesis: contradiction
then  0 <> ||.x.|| by NORMSP_0:def_5;
then  0 < ||.x.|| by CLVECT_1:105;
hence  contradiction by A1; ::_thesis: verum
end;
hence  x = 0. X ; ::_thesis: verum
end;

Lm4:  for X being ComplexNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
proof
let X be ComplexNormSpace; ::_thesis: for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
let x, y be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds
||.(x - y).|| < e ) implies x = y )
assume  for e being Real st e > 0 holds
||.(x - y).|| < e ; ::_thesis: x = y
then  x - y = 0. X by Lm3;
hence  x = y by RLVECT_1:21; ::_thesis: verum
end;

theorem Th40: :: NCFCONT2:40
for X being ComplexBanachSpace
for f being Function of X,X st f is Contraction of X holds
ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
proof
let X be ComplexBanachSpace; ::_thesis: for f being Function of X,X st f is Contraction of X holds
ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
set x0 = the Element of X;
let f be Function of X,X; ::_thesis: ( f is Contraction of X implies ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) ) )
assume  f is Contraction of X ; ::_thesis: ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
then consider K being Real such that
A1: 0 < K and
A2: K < 1 and
A3: for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= K * ||.(x - y).|| by Def7;
deffunc H1( set , set ) ->  set = f . $2;
consider g being Function such that
A4: ( dom g = NAT & g . 0 = the Element of X & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) ) from NAT_1:sch_11();
defpred S1[ Element of NAT ] means g . $1 in the carrier of X;
A5: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; ::_thesis: S1[k + 1]
 g . (k + 1) = f . (g . k) by A4;
hence  S1[k + 1] by A6, FUNCT_2:5; ::_thesis: verum
end;
A7: S1[ 0 ] by A4;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A5);
then  for n being set st n in NAT holds
g . n in the carrier of X ;
then reconsider g = g as sequence of X by A4, FUNCT_2:3;
A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(((g_^\_1)_._n)_-_(f_._(lim_g))).||_<=_K_*_||.((g_._n)_-_(lim_g)).||
let n be Element of NAT ; ::_thesis: ||.(((g ^\ 1) . n) - (f . (lim g))).|| <= K * ||.((g . n) - (lim g)).||
||.(((g ^\ 1) . n) - (f . (lim g))).|| = ||.((g . (n + 1)) - (f . (lim g))).|| by NAT_1:def_3
.= ||.((f . (g . n)) - (f . (lim g))).|| by A4 ;
hence  ||.(((g ^\ 1) . n) - (f . (lim g))).|| <= K * ||.((g . n) - (lim g)).|| by A3; ::_thesis: verum
end;
A9: for n being Element of NAT holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n)
proof
defpred S2[ Element of NAT ] means ||.((g . ($1 + 1)) - (g . $1)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power $1);
A10: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume  S2[k] ; ::_thesis: S2[k + 1]
then A11: K * ||.((g . (k + 1)) - (g . k)).|| <= K * (||.((g . 1) - (g . 0)).|| * (K to_power k)) by A1, XREAL_1:64;
 ||.((f . (g . (k + 1))) - (f . (g . k))).|| <= K * ||.((g . (k + 1)) - (g . k)).|| by A3;
then  ||.((f . (g . (k + 1))) - (f . (g . k))).|| <= ||.((g . 1) - (g . 0)).|| * (K * (K to_power k)) by A11, XXREAL_0:2;
then A12: ||.((f . (g . (k + 1))) - (f . (g . k))).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power 1) * (K to_power k)) by POWER:25;
 ( g . ((k + 1) + 1) = f . (g . (k + 1)) & g . (k + 1) = f . (g . k) ) by A4;
hence  S2[k + 1] by A1, A12, POWER:27; ::_thesis: verum
end;
||.((g . (0 + 1)) - (g . 0)).|| = ||.((g . 1) - (g . 0)).|| * 1
.= ||.((g . 1) - (g . 0)).|| * (K to_power 0) by POWER:24 ;
then A13: S2[ 0 ] ;
 for n being Element of NAT holds S2[n] from NAT_1:sch_1(A13, A10);
hence  for n being Element of NAT holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n) ; ::_thesis: verum
end;
A14: for k, n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))
proof
defpred S2[ Element of NAT ] means  for n being Element of NAT holds ||.((g . (n + $1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + $1))) / (1 - K));
A15: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_
S2[k_+_1]
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A16: S2[k] ; ::_thesis: S2[k + 1]
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((g_._(n_+_(k_+_1)))_-_(g_._n)).||_<=_||.((g_._1)_-_(g_._0)).||_*_(((K_to_power_n)_-_(K_to_power_(n_+_(k_+_1))))_/_(1_-_K))
let n be Element of NAT ; ::_thesis: ||.((g . (n + (k + 1))) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + (k + 1)))) / (1 - K))
 1 - K <> 0 by A2;
then A17: (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + (||.((g . 1) - (g . 0)).|| * (K to_power (n + k))) = (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + (((||.((g . 1) - (g . 0)).|| * (K to_power (n + k))) * (1 - K)) / (1 - K)) by XCMPLX_1:89
.= (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + ((||.((g . 1) - (g . 0)).|| * ((K to_power (n + k)) * (1 - K))) / (1 - K))
.= (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + (||.((g . 1) - (g . 0)).|| * (((K to_power (n + k)) * (1 - K)) / (1 - K))) by XCMPLX_1:74
.= ||.((g . 1) - (g . 0)).|| * ((((K to_power n) - (K to_power (n + k))) / (1 - K)) + (((K to_power (n + k)) * (1 - K)) / (1 - K)))
.= ||.((g . 1) - (g . 0)).|| * ((((K to_power n) - (K to_power (n + k))) + ((1 * (K to_power (n + k))) - (K * (K to_power (n + k))))) / (1 - K)) by XCMPLX_1:62
.= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K * (K to_power (n + k)))) / (1 - K))
.= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - ((K to_power 1) * (K to_power (n + k)))) / (1 - K)) by POWER:25
.= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power ((n + k) + 1))) / (1 - K)) by A1, POWER:27 ;
 ( ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)) & ||.((g . ((n + k) + 1)) - (g . (n + k))).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power (n + k)) ) by A9, A16;
then  ( ||.((g . (n + (k + 1))) - (g . n)).|| <= ||.((g . (n + (k + 1))) - (g . (n + k))).|| + ||.((g . (n + k)) - (g . n)).|| & ||.((g . (n + (k + 1))) - (g . (n + k))).|| + ||.((g . (n + k)) - (g . n)).|| <= (||.((g . 1) - (g . 0)).|| * (K to_power (n + k))) + (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) ) by CLVECT_1:111, XREAL_1:7;
hence  ||.((g . (n + (k + 1))) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + (k + 1)))) / (1 - K)) by A17, XXREAL_0:2; ::_thesis: verum
end;
hence  S2[k + 1] ; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((g_._(n_+_0))_-_(g_._n)).||_<=_||.((g_._1)_-_(g_._0)).||_*_(((K_to_power_n)_-_(K_to_power_(n_+_0)))_/_(1_-_K))
let n be Element of NAT ; ::_thesis: ||.((g . (n + 0)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + 0))) / (1 - K))
||.((g . (n + 0)) - (g . n)).|| = ||.(0. X).|| by RLVECT_1:15
.= 0 by CLVECT_1:102 ;
hence  ||.((g . (n + 0)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + 0))) / (1 - K)) ; ::_thesis: verum
end;
then A18: S2[ 0 ] ;
 for k being Element of NAT holds S2[k] from NAT_1:sch_1(A18, A15);
hence  for k, n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)) ; ::_thesis: verum
end;
A19: for k, n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
proof
let k be Element of NAT ; ::_thesis: for n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((g_._(n_+_k))_-_(g_._n)).||_<=_||.((g_._1)_-_(g_._0)).||_*_((K_to_power_n)_/_(1_-_K))
let n be Element of NAT ; ::_thesis: ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
A20: 0 <= ||.((g . 1) - (g . 0)).|| by CLVECT_1:105;
 K to_power (n + k) > 0 by A1, POWER:34;
then A21: (K to_power n) - (K to_power (n + k)) <= (K to_power n) - 0 by XREAL_1:13;
 1 - K > 1 - 1 by A2, XREAL_1:15;
then  ((K to_power n) - (K to_power (n + k))) / (1 - K) <= (K to_power n) / (1 - K) by A21, XREAL_1:72;
then A22: ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)) <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A20, XREAL_1:64;
 ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)) by A14;
hence  ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A22, XXREAL_0:2; ::_thesis: verum
end;
hence  for n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) ; ::_thesis: verum
end;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_nn_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_nn_&_m_>=_nn_holds_
||.((g_._n)_-_(g_._m)).||_<_e
let e be Real; ::_thesis: ( e > 0 implies ex nn being Element of NAT st
for n, m being Element of NAT st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e )
assume A23: e > 0 ; ::_thesis: ex nn being Element of NAT st
for n, m being Element of NAT st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e
 e / 2 > 0 by A23, XREAL_1:215;
then consider n being Element of NAT  such that
A24: abs ((||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n)) < e / 2 by A1, A2, NFCONT_2:16;
take nn = n + 1; ::_thesis: for n, m being Element of NAT st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e
 (||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n) <= abs ((||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n)) by ABSVALUE:4;
then  (||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n) < e / 2 by A24, XXREAL_0:2;
then A25: ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) < e / 2 by XCMPLX_1:75;
now__::_thesis:_for_m,_l_being_Element_of_NAT_st_nn_<=_m_&_nn_<=_l_holds_
||.((g_._l)_-_(g_._m)).||_<_e
let m, l be Element of NAT ; ::_thesis: ( nn <= m & nn <= l implies ||.((g . l) - (g . m)).|| < e )
assume that
A26: nn <= m and
A27: nn <= l ; ::_thesis: ||.((g . l) - (g . m)).|| < e
 n < m by A26, NAT_1:13;
then consider k1 being Nat such that
A28: n + k1 = m by NAT_1:10;
 n < l by A27, NAT_1:13;
then consider k2 being Nat such that
A29: n + k2 = l by NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def_12;
 ||.((g . (n + k2)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A19;
then A30: ||.((g . l) - (g . n)).|| < e / 2 by A25, A29, XXREAL_0:2;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12;
 ||.((g . (n + k1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A19;
then  ||.((g . m) - (g . n)).|| < e / 2 by A25, A28, XXREAL_0:2;
hence  ||.((g . l) - (g . m)).|| < e by A30, Lm2; ::_thesis: verum
end;
hence  for n, m being Element of NAT st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e ; ::_thesis: verum
end;
then  g is Cauchy_sequence_by_Norm by CSSPACE3:8;
then A31: g is convergent by CLOPBAN1:def_13;
then A32: K (#) ||.(g - (lim g)).|| is convergent by CLVECT_1:118, SEQ_2:7;
A33: lim (K (#) ||.(g - (lim g)).||) = K * (lim ||.(g - (lim g)).||) by A31, CLVECT_1:118, SEQ_2:8
.= K * 0 by A31, CLVECT_1:118
.= 0 ;
A34: for e being Real st e > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((g ^\ 1) . m) - (f . (lim g))).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((g ^\ 1) . m) - (f . (lim g))).|| < e )
assume  e > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((g ^\ 1) . m) - (f . (lim g))).|| < e
then consider n being Element of NAT  such that
A35: for m being Element of NAT st n <= m holds
abs (((K (#) ||.(g - (lim g)).||) . m) - 0) < e by A32, A33, SEQ_2:def_7;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
||.(((g ^\ 1) . m) - (f . (lim g))).|| < e
now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((g_^\_1)_._m)_-_(f_._(lim_g))).||_<_e
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e )
assume  n <= m ; ::_thesis: ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e
then  abs (((K (#) ||.(g - (lim g)).||) . m) - 0) < e by A35;
then  abs (K * (||.(g - (lim g)).|| . m)) < e by SEQ_1:9;
then  abs (K * ||.((g - (lim g)) . m).||) < e by NORMSP_0:def_4;
then A36: abs (K * ||.((g . m) - (lim g)).||) < e by NORMSP_1:def_4;
 K * ||.((g . m) - (lim g)).|| <= abs (K * ||.((g . m) - (lim g)).||) by ABSVALUE:4;
then A37: K * ||.((g . m) - (lim g)).|| < e by A36, XXREAL_0:2;
 ||.(((g ^\ 1) . m) - (f . (lim g))).|| <= K * ||.((g . m) - (lim g)).|| by A8;
hence  ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e by A37, XXREAL_0:2; ::_thesis: verum
end;
hence  for m being Element of NAT st n <= m holds
||.(((g ^\ 1) . m) - (f . (lim g))).|| < e ; ::_thesis: verum
end;
take xp = lim g; ::_thesis: ( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
A38: ( g ^\ 1 is convergent & lim (g ^\ 1) = lim g ) by A31, CLOPBAN3:9;
then A39: lim g = f . (lim g) by A34, CLVECT_1:def_16;
now__::_thesis:_for_x_being_Point_of_X_st_f_._x_=_x_holds_
x_=_xp
let x be Point of X; ::_thesis: ( f . x = x implies x = xp )
assume A40: f . x = x ; ::_thesis: x = xp
A41: for k being Element of NAT holds ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power k)
proof
defpred S2[ Element of NAT ] means ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power $1);
A42: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume  S2[k] ; ::_thesis: S2[k + 1]
then A43: K * ||.(x - xp).|| <= K * (||.(x - xp).|| * (K to_power k)) by A1, XREAL_1:64;
 ||.((f . x) - (f . xp)).|| <= K * ||.(x - xp).|| by A3;
then  ||.((f . x) - (f . xp)).|| <= ||.(x - xp).|| * (K * (K to_power k)) by A43, XXREAL_0:2;
then  ||.((f . x) - (f . xp)).|| <= ||.(x - xp).|| * ((K to_power 1) * (K to_power k)) by POWER:25;
hence  S2[k + 1] by A1, A39, A40, POWER:27; ::_thesis: verum
end;
||.(x - xp).|| = ||.(x - xp).|| * 1
.= ||.(x - xp).|| * (K to_power 0) by POWER:24 ;
then A44: S2[ 0 ] ;
 for n being Element of NAT holds S2[n] from NAT_1:sch_1(A44, A42);
hence  for k being Element of NAT holds ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power k) ; ::_thesis: verum
end;
 for e being Real st 0 < e holds
||.(x - xp).|| < e
proof
let e be Real; ::_thesis: ( 0 < e implies ||.(x - xp).|| < e )
assume  0 < e ; ::_thesis: ||.(x - xp).|| < e
then consider n being Element of NAT  such that
A45: abs (||.(x - xp).|| * (K to_power n)) < e by A1, A2, NFCONT_2:16;
 ||.(x - xp).|| * (K to_power n) <= abs (||.(x - xp).|| * (K to_power n)) by ABSVALUE:4;
then A46: ||.(x - xp).|| * (K to_power n) < e by A45, XXREAL_0:2;
 ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power n) by A41;
hence  ||.(x - xp).|| < e by A46, XXREAL_0:2; ::_thesis: verum
end;
hence  x = xp by Lm4; ::_thesis: verum
end;
hence  ( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) ) by A38, A34, CLVECT_1:def_16; ::_thesis: verum
end;

theorem :: NCFCONT2:41
for X being ComplexBanachSpace
for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is Contraction of X holds
ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
proof
let X be ComplexBanachSpace; ::_thesis: for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is Contraction of X holds
ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
let f be Function of X,X; ::_thesis: ( ex n0 being Element of NAT st iter (f,n0) is Contraction of X implies ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) ) )
given n0 being Element of NAT  such that A1: iter (f,n0) is Contraction of X ; ::_thesis: ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
consider xp being Point of X such that
A2: (iter (f,n0)) . xp = xp and
A3: for x being Point of X st (iter (f,n0)) . x = x holds
xp = x by A1, Th40;
A4: now__::_thesis:_for_x_being_Point_of_X_st_f_._x_=_x_holds_
xp_=_x
let x be Point of X; ::_thesis: ( f . x = x implies xp = x )
assume A5: f . x = x ; ::_thesis: xp = x
 for n being Element of NAT holds (iter (f,n)) . x = x
proof
defpred S1[ Element of NAT ] means (iter (f,$1)) . x = x;
A6: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; ::_thesis: S1[n + 1]
A8: iter (f,n) is Function of X,X by FUNCT_7:83;
(iter (f,(n + 1))) . x = (f * (iter (f,n))) . x by FUNCT_7:71
.= x by A5, A7, A8, FUNCT_2:15 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(iter (f,0)) . x = (id the carrier of X) . x by FUNCT_7:84
.= x by FUNCT_1:17 ;
then A9: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A6);
hence  for n being Element of NAT holds (iter (f,n)) . x = x ; ::_thesis: verum
end;
then  (iter (f,n0)) . x = x ;
hence  xp = x by A3; ::_thesis: verum
end;
A10: iter (f,n0) is Function of X,X by FUNCT_7:83;
(iter (f,n0)) . (f . xp) = ((iter (f,n0)) * f) . xp by FUNCT_2:15
.= (iter (f,(n0 + 1))) . xp by FUNCT_7:69
.= (f * (iter (f,n0))) . xp by FUNCT_7:71
.= f . xp by A2, A10, FUNCT_2:15 ;
then  f . xp = xp by A3;
hence  ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) ) by A4; ::_thesis: verum
end;