:: Continuous Functions on Real and Complex Normed Linear Spaces
:: by Noboru Endou
::
:: Received August 20, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: NCFCONT1:1
for CNS being ComplexNormSpace
for seq being sequence of CNS holds - seq = (- 1r) * seq
proofend;

definition
let CNS be ComplexNormSpace;
let x0 be Point of CNS;
mode Neighbourhood of x0 ->  Subset of CNS means :Def1: :: NCFCONT1:def 1
 ex g being Real st
( 0 < g &amp;  {  y where y is Point of CNS : ||.(y - x0).|| < g  }  c= it );
existence
 ex b1 being Subset of CNS ex g being Real st
( 0 < g &amp;  {  y where y is Point of CNS : ||.(y - x0).|| < g  }  c= b1 )
proofend;
end;

:: deftheorem Def1 defines Neighbourhood NCFCONT1:def_1_:_
 for CNS being ComplexNormSpace
for x0 being Point of CNS
for b3 being Subset of CNS holds
( b3 is Neighbourhood of x0 iff ex g being Real st
( 0 < g &amp;  {  y where y is Point of CNS : ||.(y - x0).|| < g  }  c= b3 ) );

theorem Th2: :: NCFCONT1:2
for CNS being ComplexNormSpace
for x0 being Point of CNS
for g being Real st 0 < g holds
{  y where y is Point of CNS : ||.(y - x0).|| < g  }  is Neighbourhood of x0
proofend;

theorem Th3: :: NCFCONT1:3
for CNS being ComplexNormSpace
for x0 being Point of CNS
for N being Neighbourhood of x0 holds x0 in N
proofend;

definition
let CNS be ComplexNormSpace;
let X be Subset of CNS;
attrX is compact  means :Def2: :: NCFCONT1:def 2
 for s1 being sequence of CNS st rng s1 c= X holds
ex s2 being sequence of CNS st
( s2 is subsequence of s1 &amp; s2 is convergent &amp; lim s2 in X );
end;

:: deftheorem Def2 defines compact NCFCONT1:def_2_:_
 for CNS being ComplexNormSpace
for X being Subset of CNS holds
( X is compact iff for s1 being sequence of CNS st rng s1 c= X holds
ex s2 being sequence of CNS st
( s2 is subsequence of s1 &amp; s2 is convergent &amp; lim s2 in X ) );

definition
let CNS be ComplexNormSpace;
let X be Subset of CNS;
attrX is closed  means :: NCFCONT1:def 3
 for s1 being sequence of CNS st rng s1 c= X &amp; s1 is convergent holds
lim s1 in X;
end;

:: deftheorem  defines closed NCFCONT1:def_3_:_
 for CNS being ComplexNormSpace
for X being Subset of CNS holds
( X is closed iff for s1 being sequence of CNS st rng s1 c= X &amp; s1 is convergent holds
lim s1 in X );

definition
let CNS be ComplexNormSpace;
let X be Subset of CNS;
attrX is open  means :: NCFCONT1:def 4
X ` is closed ;
end;

:: deftheorem  defines open NCFCONT1:def_4_:_
 for CNS being ComplexNormSpace
for X being Subset of CNS holds
( X is open iff X ` is closed );

definition
let CNS1, CNS2 be ComplexNormSpace;
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
predf is_continuous_in x0 means :Def5: :: NCFCONT1:def 5
( x0 in dom f &amp; ( for seq being sequence of CNS1 st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) );
end;

:: deftheorem Def5 defines is_continuous_in NCFCONT1:def_5_:_
 for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for seq being sequence of CNS1 st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) ) );

definition
let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
predf is_continuous_in x0 means :Def6: :: NCFCONT1:def 6
( x0 in dom f &amp; ( for seq being sequence of CNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) );
end;

:: deftheorem Def6 defines is_continuous_in NCFCONT1:def_6_:_
 for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for seq being sequence of CNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) ) );

definition
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
predf is_continuous_in x0 means :Def7: :: NCFCONT1:def 7
( x0 in dom f &amp; ( for seq being sequence of RNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) );
end;

:: deftheorem Def7 defines is_continuous_in NCFCONT1:def_7_:_
 for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for seq being sequence of RNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) ) );

definition
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,COMPLEX;
let x0 be Point of CNS;
predf is_continuous_in x0 means :Def8: :: NCFCONT1:def 8
( x0 in dom f &amp; ( for seq being sequence of CNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) );
end;

:: deftheorem Def8 defines is_continuous_in NCFCONT1:def_8_:_
 for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX
for x0 being Point of CNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for seq being sequence of CNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) ) );

definition
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,REAL;
let x0 be Point of CNS;
predf is_continuous_in x0 means :Def9: :: NCFCONT1:def 9
( x0 in dom f &amp; ( for seq being sequence of CNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) );
end;

:: deftheorem Def9 defines is_continuous_in NCFCONT1:def_9_:_
 for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL
for x0 being Point of CNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for seq being sequence of CNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) ) );

definition
let RNS be RealNormSpace;
let f be PartFunc of the carrier of RNS,COMPLEX;
let x0 be Point of RNS;
predf is_continuous_in x0 means :Def10: :: NCFCONT1:def 10
( x0 in dom f &amp; ( for seq being sequence of RNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) );
end;

:: deftheorem Def10 defines is_continuous_in NCFCONT1:def_10_:_
 for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX
for x0 being Point of RNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for seq being sequence of RNS st rng seq c= dom f &amp; seq is convergent &amp; lim seq = x0 holds
( f /* seq is convergent &amp; f /. x0 = lim (f /* seq) ) ) ) );

theorem Th4: :: NCFCONT1:4
for n being Element of NAT
for CNS1, CNS2 being ComplexNormSpace
for seq being sequence of CNS1
for h being PartFunc of CNS1,CNS2 st rng seq c= dom h holds
seq . n in dom h
proofend;

theorem Th5: :: NCFCONT1:5
for n being Element of NAT
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for seq being sequence of CNS
for h being PartFunc of CNS,RNS st rng seq c= dom h holds
seq . n in dom h
proofend;

theorem Th6: :: NCFCONT1:6
for n being Element of NAT
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for seq being sequence of RNS
for h being PartFunc of RNS,CNS st rng seq c= dom h holds
seq . n in dom h
proofend;

theorem Th7: :: NCFCONT1:7
for CNS being ComplexNormSpace
for seq being sequence of CNS
for x being set holds
( x in rng seq iff ex n being Element of NAT st x = seq . n )
proofend;

theorem Th8: :: NCFCONT1:8
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of CNS1 st x1 in dom f &amp; ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
proofend;

theorem Th9: :: NCFCONT1:9
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of CNS st x1 in dom f &amp; ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
proofend;

theorem Th10: :: NCFCONT1:10
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of RNS st x1 in dom f &amp; ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
proofend;

theorem Th11: :: NCFCONT1:11
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL
for x0 being Point of CNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of CNS st x1 in dom f &amp; ||.(x1 - x0).|| < s holds
abs ((f /. x1) - (f /. x0)) < r ) ) ) ) )
proofend;

theorem Th12: :: NCFCONT1:12
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX
for x0 being Point of CNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of CNS st x1 in dom f &amp; ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proofend;

theorem Th13: :: NCFCONT1:13
for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX
for x0 being Point of RNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of RNS st x1 in dom f &amp; ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proofend;

theorem Th14: :: NCFCONT1:14
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Point of CNS1 st x1 in dom f &amp; x1 in N holds
f /. x1 in N1 ) ) )
proofend;

theorem Th15: :: NCFCONT1:15
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Point of CNS st x1 in dom f &amp; x1 in N holds
f /. x1 in N1 ) ) )
proofend;

theorem Th16: :: NCFCONT1:16
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Point of RNS st x1 in dom f &amp; x1 in N holds
f /. x1 in N1 ) ) )
proofend;

theorem Th17: :: NCFCONT1:17
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )
proofend;

theorem Th18: :: NCFCONT1:18
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )
proofend;

theorem Th19: :: NCFCONT1:19
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )
proofend;

theorem :: NCFCONT1:20
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 st x0 in dom f &amp; ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
proofend;

theorem :: NCFCONT1:21
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS st x0 in dom f &amp; ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
proofend;

theorem :: NCFCONT1:22
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS st x0 in dom f &amp; ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
proofend;

theorem Th23: :: NCFCONT1:23
for CNS1, CNS2 being ComplexNormSpace
for h1, h2 being PartFunc of CNS1,CNS2
for seq being sequence of CNS1 st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) &amp; (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
proofend;

theorem Th24: :: NCFCONT1:24
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h1, h2 being PartFunc of CNS,RNS
for seq being sequence of CNS st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) &amp; (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
proofend;

theorem Th25: :: NCFCONT1:25
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h1, h2 being PartFunc of RNS,CNS
for seq being sequence of RNS st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) &amp; (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
proofend;

theorem Th26: :: NCFCONT1:26
for CNS1, CNS2 being ComplexNormSpace
for h being PartFunc of CNS1,CNS2
for seq being sequence of CNS1
for z being Complex st rng seq c= dom h holds
(z (#) h) /* seq = z * (h /* seq)
proofend;

theorem Th27: :: NCFCONT1:27
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h being PartFunc of CNS,RNS
for seq being sequence of CNS
for r being Real st rng seq c= dom h holds
(r (#) h) /* seq = r * (h /* seq)
proofend;

theorem Th28: :: NCFCONT1:28
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h being PartFunc of RNS,CNS
for seq being sequence of RNS
for z being Complex st rng seq c= dom h holds
(z (#) h) /* seq = z * (h /* seq)
proofend;

theorem Th29: :: NCFCONT1:29
for CNS1, CNS2 being ComplexNormSpace
for h being PartFunc of CNS1,CNS2
for seq being sequence of CNS1 st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq &amp; - (h /* seq) = (- h) /* seq )
proofend;

theorem Th30: :: NCFCONT1:30
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h being PartFunc of CNS,RNS
for seq being sequence of CNS st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq &amp; - (h /* seq) = (- h) /* seq )
proofend;

theorem Th31: :: NCFCONT1:31
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h being PartFunc of RNS,CNS
for seq being sequence of RNS st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq &amp; - (h /* seq) = (- h) /* seq )
proofend;

theorem :: NCFCONT1:32
for CNS1, CNS2 being ComplexNormSpace
for f1, f2 being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 st f1 is_continuous_in x0 &amp; f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 &amp; f1 - f2 is_continuous_in x0 )
proofend;

theorem :: NCFCONT1:33
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f1, f2 being PartFunc of CNS,RNS
for x0 being Point of CNS st f1 is_continuous_in x0 &amp; f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 &amp; f1 - f2 is_continuous_in x0 )
proofend;

theorem :: NCFCONT1:34
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f1, f2 being PartFunc of RNS,CNS
for x0 being Point of RNS st f1 is_continuous_in x0 &amp; f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 &amp; f1 - f2 is_continuous_in x0 )
proofend;

theorem Th35: :: NCFCONT1:35
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1
for z being Complex st f is_continuous_in x0 holds
z (#) f is_continuous_in x0
proofend;

theorem Th36: :: NCFCONT1:36
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS
for r being Real st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
proofend;

theorem Th37: :: NCFCONT1:37
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS
for z being Complex st f is_continuous_in x0 holds
z (#) f is_continuous_in x0
proofend;

theorem :: NCFCONT1:38
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 &amp; - f is_continuous_in x0 )
proofend;

theorem :: NCFCONT1:39
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 &amp; - f is_continuous_in x0 )
proofend;

theorem :: NCFCONT1:40
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 &amp; - f is_continuous_in x0 )
proofend;

definition
let CNS1, CNS2 be ComplexNormSpace;
let f be PartFunc of CNS1,CNS2;
let X be set ;
predf is_continuous_on X means :Def11: :: NCFCONT1:def 11
( X c= dom f &amp; ( for x0 being Point of CNS1 st x0 in X holds
f | X is_continuous_in x0 ) );
end;

:: deftheorem Def11 defines is_continuous_on NCFCONT1:def_11_:_
 for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for X being set holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of CNS1 st x0 in X holds
f | X is_continuous_in x0 ) ) );

definition
let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let f be PartFunc of CNS,RNS;
let X be set ;
predf is_continuous_on X means :Def12: :: NCFCONT1:def 12
( X c= dom f &amp; ( for x0 being Point of CNS st x0 in X holds
f | X is_continuous_in x0 ) );
end;

:: deftheorem Def12 defines is_continuous_on NCFCONT1:def_12_:_
 for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for X being set holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of CNS st x0 in X holds
f | X is_continuous_in x0 ) ) );

definition
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let g be PartFunc of RNS,CNS;
let X be set ;
predg is_continuous_on X means :Def13: :: NCFCONT1:def 13
( X c= dom g &amp; ( for x0 being Point of RNS st x0 in X holds
g | X is_continuous_in x0 ) );
end;

:: deftheorem Def13 defines is_continuous_on NCFCONT1:def_13_:_
 for RNS being RealNormSpace
for CNS being ComplexNormSpace
for g being PartFunc of RNS,CNS
for X being set holds
( g is_continuous_on X iff ( X c= dom g &amp; ( for x0 being Point of RNS st x0 in X holds
g | X is_continuous_in x0 ) ) );

definition
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,COMPLEX;
let X be set ;
predf is_continuous_on X means :Def14: :: NCFCONT1:def 14
( X c= dom f &amp; ( for x0 being Point of CNS st x0 in X holds
f | X is_continuous_in x0 ) );
end;

:: deftheorem Def14 defines is_continuous_on NCFCONT1:def_14_:_
 for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX
for X being set holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of CNS st x0 in X holds
f | X is_continuous_in x0 ) ) );

definition
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,REAL;
let X be set ;
predf is_continuous_on X means :Def15: :: NCFCONT1:def 15
( X c= dom f &amp; ( for x0 being Point of CNS st x0 in X holds
f | X is_continuous_in x0 ) );
end;

:: deftheorem Def15 defines is_continuous_on NCFCONT1:def_15_:_
 for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL
for X being set holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of CNS st x0 in X holds
f | X is_continuous_in x0 ) ) );

definition
let RNS be RealNormSpace;
let f be PartFunc of the carrier of RNS,COMPLEX;
let X be set ;
predf is_continuous_on X means :Def16: :: NCFCONT1:def 16
( X c= dom f &amp; ( for x0 being Point of RNS st x0 in X holds
f | X is_continuous_in x0 ) );
end;

:: deftheorem Def16 defines is_continuous_on NCFCONT1:def_16_:_
 for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX
for X being set holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of RNS st x0 in X holds
f | X is_continuous_in x0 ) ) );

theorem Th41: :: NCFCONT1:41
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for s1 being sequence of CNS1 st rng s1 c= X &amp; s1 is convergent &amp; lim s1 in X holds
( f /* s1 is convergent &amp; f /. (lim s1) = lim (f /* s1) ) ) ) )
proofend;

theorem Th42: :: NCFCONT1:42
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for s1 being sequence of CNS st rng s1 c= X &amp; s1 is convergent &amp; lim s1 in X holds
( f /* s1 is convergent &amp; f /. (lim s1) = lim (f /* s1) ) ) ) )
proofend;

theorem Th43: :: NCFCONT1:43
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for s1 being sequence of RNS st rng s1 c= X &amp; s1 is convergent &amp; lim s1 in X holds
( f /* s1 is convergent &amp; f /. (lim s1) = lim (f /* s1) ) ) ) )
proofend;

theorem Th44: :: NCFCONT1:44
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of CNS1
for r being Real st x0 in X &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of CNS1 st x1 in X &amp; ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
proofend;

theorem Th45: :: NCFCONT1:45
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of CNS
for r being Real st x0 in X &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of CNS st x1 in X &amp; ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
proofend;

theorem Th46: :: NCFCONT1:46
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of RNS
for r being Real st x0 in X &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of RNS st x1 in X &amp; ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
proofend;

theorem :: NCFCONT1:47
for CNS being ComplexNormSpace
for X being set
for f being PartFunc of the carrier of CNS,COMPLEX holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of CNS
for r being Real st x0 in X &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of CNS st x1 in X &amp; ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proofend;

theorem :: NCFCONT1:48
for CNS being ComplexNormSpace
for X being set
for f being PartFunc of the carrier of CNS,REAL holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of CNS
for r being Real st x0 in X &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of CNS st x1 in X &amp; ||.(x1 - x0).|| < s holds
abs ((f /. x1) - (f /. x0)) < r ) ) ) ) )
proofend;

theorem :: NCFCONT1:49
for RNS being RealNormSpace
for X being set
for f being PartFunc of the carrier of RNS,COMPLEX holds
( f is_continuous_on X iff ( X c= dom f &amp; ( for x0 being Point of RNS
for r being Real st x0 in X &amp; 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1 being Point of RNS st x1 in X &amp; ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proofend;

theorem :: NCFCONT1:50
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 holds
( f is_continuous_on X iff f | X is_continuous_on X )
proofend;

theorem :: NCFCONT1:51
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS holds
( f is_continuous_on X iff f | X is_continuous_on X )
proofend;

theorem :: NCFCONT1:52
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS holds
( f is_continuous_on X iff f | X is_continuous_on X )
proofend;

theorem :: NCFCONT1:53
for CNS being ComplexNormSpace
for X being set
for f being PartFunc of the carrier of CNS,COMPLEX holds
( f is_continuous_on X iff f | X is_continuous_on X )
proofend;

theorem Th54: :: NCFCONT1:54
for CNS being ComplexNormSpace
for X being set
for f being PartFunc of the carrier of CNS,REAL holds
( f is_continuous_on X iff f | X is_continuous_on X )
proofend;

theorem :: NCFCONT1:55
for RNS being RealNormSpace
for X being set
for f being PartFunc of the carrier of RNS,COMPLEX holds
( f is_continuous_on X iff f | X is_continuous_on X )
proofend;

theorem Th56: :: NCFCONT1:56
for CNS1, CNS2 being ComplexNormSpace
for X, X1 being set
for f being PartFunc of CNS1,CNS2 st f is_continuous_on X &amp; X1 c= X holds
f is_continuous_on X1
proofend;

theorem Th57: :: NCFCONT1:57
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f being PartFunc of CNS,RNS st f is_continuous_on X &amp; X1 c= X holds
f is_continuous_on X1
proofend;

theorem Th58: :: NCFCONT1:58
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f being PartFunc of RNS,CNS st f is_continuous_on X &amp; X1 c= X holds
f is_continuous_on X1
proofend;

theorem :: NCFCONT1:59
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 st x0 in dom f holds
f is_continuous_on {x0}
proofend;

theorem :: NCFCONT1:60
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS st x0 in dom f holds
f is_continuous_on {x0}
proofend;

theorem :: NCFCONT1:61
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS st x0 in dom f holds
f is_continuous_on {x0}
proofend;

theorem Th62: :: NCFCONT1:62
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_continuous_on X &amp; f2 is_continuous_on X holds
( f1 + f2 is_continuous_on X &amp; f1 - f2 is_continuous_on X )
proofend;

theorem Th63: :: NCFCONT1:63
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f1, f2 being PartFunc of CNS,RNS st f1 is_continuous_on X &amp; f2 is_continuous_on X holds
( f1 + f2 is_continuous_on X &amp; f1 - f2 is_continuous_on X )
proofend;

theorem Th64: :: NCFCONT1:64
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f1, f2 being PartFunc of RNS,CNS st f1 is_continuous_on X &amp; f2 is_continuous_on X holds
( f1 + f2 is_continuous_on X &amp; f1 - f2 is_continuous_on X )
proofend;

theorem :: NCFCONT1:65
for CNS1, CNS2 being ComplexNormSpace
for X, X1 being set
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_continuous_on X &amp; f2 is_continuous_on X1 holds
( f1 + f2 is_continuous_on X /\ X1 &amp; f1 - f2 is_continuous_on X /\ X1 )
proofend;

theorem :: NCFCONT1:66
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of CNS,RNS st f1 is_continuous_on X &amp; f2 is_continuous_on X1 holds
( f1 + f2 is_continuous_on X /\ X1 &amp; f1 - f2 is_continuous_on X /\ X1 )
proofend;

theorem :: NCFCONT1:67
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of RNS,CNS st f1 is_continuous_on X &amp; f2 is_continuous_on X1 holds
( f1 + f2 is_continuous_on X /\ X1 &amp; f1 - f2 is_continuous_on X /\ X1 )
proofend;

theorem Th68: :: NCFCONT1:68
for z being Complex
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 st f is_continuous_on X holds
z (#) f is_continuous_on X
proofend;

theorem Th69: :: NCFCONT1:69
for r being Real
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st f is_continuous_on X holds
r (#) f is_continuous_on X
proofend;

theorem Th70: :: NCFCONT1:70
for z being Complex
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS st f is_continuous_on X holds
z (#) f is_continuous_on X
proofend;

theorem Th71: :: NCFCONT1:71
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 st f is_continuous_on X holds
( ||.f.|| is_continuous_on X &amp; - f is_continuous_on X )
proofend;

theorem Th72: :: NCFCONT1:72
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st f is_continuous_on X holds
( ||.f.|| is_continuous_on X &amp; - f is_continuous_on X )
proofend;

theorem Th73: :: NCFCONT1:73
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS st f is_continuous_on X holds
( ||.f.|| is_continuous_on X &amp; - f is_continuous_on X )
proofend;

theorem :: NCFCONT1:74
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is total &amp; ( for x1, x2 being Point of CNS1 holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) &amp; ex x0 being Point of CNS1 st f is_continuous_in x0 holds
f is_continuous_on the carrier of CNS1
proofend;

theorem :: NCFCONT1:75
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS st f is total &amp; ( for x1, x2 being Point of CNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) &amp; ex x0 being Point of CNS st f is_continuous_in x0 holds
f is_continuous_on the carrier of CNS
proofend;

theorem :: NCFCONT1:76
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS st f is total &amp; ( for x1, x2 being Point of RNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) &amp; ex x0 being Point of RNS st f is_continuous_in x0 holds
f is_continuous_on the carrier of RNS
proofend;

theorem Th77: :: NCFCONT1:77
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st dom f is compact &amp; f is_continuous_on dom f holds
rng f is compact
proofend;

theorem Th78: :: NCFCONT1:78
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS st dom f is compact &amp; f is_continuous_on dom f holds
rng f is compact
proofend;

theorem Th79: :: NCFCONT1:79
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS st dom f is compact &amp; f is_continuous_on dom f holds
rng f is compact
proofend;

theorem :: NCFCONT1:80
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX st dom f is compact &amp; f is_continuous_on dom f holds
rng f is compact
proofend;

theorem Th81: :: NCFCONT1:81
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL st dom f is compact &amp; f is_continuous_on dom f holds
rng f is compact
proofend;

theorem :: NCFCONT1:82
for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX st dom f is compact &amp; f is_continuous_on dom f holds
rng f is compact
proofend;

theorem :: NCFCONT1:83
for CNS1, CNS2 being ComplexNormSpace
for Y being Subset of CNS1
for f being PartFunc of CNS1,CNS2 st Y c= dom f &amp; Y is compact &amp; f is_continuous_on Y holds
f .: Y is compact
proofend;

theorem :: NCFCONT1:84
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for Y being Subset of CNS
for f being PartFunc of CNS,RNS st Y c= dom f &amp; Y is compact &amp; f is_continuous_on Y holds
f .: Y is compact
proofend;

theorem :: NCFCONT1:85
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for Y being Subset of RNS
for f being PartFunc of RNS,CNS st Y c= dom f &amp; Y is compact &amp; f is_continuous_on Y holds
f .: Y is compact
proofend;

theorem Th86: :: NCFCONT1:86
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL st dom f <> {} &amp; dom f is compact &amp; f is_continuous_on dom f holds
ex x1, x2 being Point of CNS st
( x1 in dom f &amp; x2 in dom f &amp; f /. x1 = upper_bound (rng f) &amp; f /. x2 = lower_bound (rng f) )
proofend;

theorem Th87: :: NCFCONT1:87
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st dom f <> {} &amp; dom f is compact &amp; f is_continuous_on dom f holds
ex x1, x2 being Point of CNS1 st
( x1 in dom f &amp; x2 in dom f &amp; ||.f.|| /. x1 = upper_bound (rng ||.f.||) &amp; ||.f.|| /. x2 = lower_bound (rng ||.f.||) )
proofend;

theorem Th88: :: NCFCONT1:88
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS st dom f <> {} &amp; dom f is compact &amp; f is_continuous_on dom f holds
ex x1, x2 being Point of CNS st
( x1 in dom f &amp; x2 in dom f &amp; ||.f.|| /. x1 = upper_bound (rng ||.f.||) &amp; ||.f.|| /. x2 = lower_bound (rng ||.f.||) )
proofend;

theorem Th89: :: NCFCONT1:89
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS st dom f <> {} &amp; dom f is compact &amp; f is_continuous_on dom f holds
ex x1, x2 being Point of RNS st
( x1 in dom f &amp; x2 in dom f &amp; ||.f.|| /. x1 = upper_bound (rng ||.f.||) &amp; ||.f.|| /. x2 = lower_bound (rng ||.f.||) )
proofend;

theorem Th90: :: NCFCONT1:90
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 holds ||.f.|| | X = ||.(f | X).||
proofend;

theorem Th91: :: NCFCONT1:91
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS holds ||.f.|| | X = ||.(f | X).||
proofend;

theorem Th92: :: NCFCONT1:92
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS holds ||.f.|| | X = ||.(f | X).||
proofend;

theorem :: NCFCONT1:93
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for Y being Subset of CNS1 st Y <> {} &amp; Y c= dom f &amp; Y is compact &amp; f is_continuous_on Y holds
ex x1, x2 being Point of CNS1 st
( x1 in Y &amp; x2 in Y &amp; ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) &amp; ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
proofend;

theorem :: NCFCONT1:94
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for Y being Subset of CNS st Y <> {} &amp; Y c= dom f &amp; Y is compact &amp; f is_continuous_on Y holds
ex x1, x2 being Point of CNS st
( x1 in Y &amp; x2 in Y &amp; ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) &amp; ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
proofend;

theorem :: NCFCONT1:95
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y <> {} &amp; Y c= dom f &amp; Y is compact &amp; f is_continuous_on Y holds
ex x1, x2 being Point of RNS st
( x1 in Y &amp; x2 in Y &amp; ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) &amp; ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) )
proofend;

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

definition
let CNS1, CNS2 be ComplexNormSpace;
let X be set ;
let f be PartFunc of CNS1,CNS2;
predf is_Lipschitzian_on X means :Def17: :: NCFCONT1:def 17
( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of CNS1 st x1 in X &amp; x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) );
end;

:: deftheorem Def17 defines is_Lipschitzian_on NCFCONT1:def_17_:_
 for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 holds
( f is_Lipschitzian_on X iff ( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of CNS1 st x1 in X &amp; x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ) );

definition
let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let X be set ;
let f be PartFunc of CNS,RNS;
predf is_Lipschitzian_on X means :Def18: :: NCFCONT1:def 18
( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) );
end;

:: deftheorem Def18 defines is_Lipschitzian_on NCFCONT1:def_18_:_
 for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS holds
( f is_Lipschitzian_on X iff ( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ) );

definition
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let X be set ;
let f be PartFunc of RNS,CNS;
predf is_Lipschitzian_on X means :Def19: :: NCFCONT1:def 19
( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of RNS st x1 in X &amp; x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) );
end;

:: deftheorem Def19 defines is_Lipschitzian_on NCFCONT1:def_19_:_
 for RNS being RealNormSpace
for CNS being ComplexNormSpace
for X being set
for f being PartFunc of RNS,CNS holds
( f is_Lipschitzian_on X iff ( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of RNS st x1 in X &amp; x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ) );

definition
let CNS be ComplexNormSpace;
let X be set ;
let f be PartFunc of the carrier of CNS,COMPLEX;
predf is_Lipschitzian_on X means :Def20: :: NCFCONT1:def 20
( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) );
end;

:: deftheorem Def20 defines is_Lipschitzian_on NCFCONT1:def_20_:_
 for CNS being ComplexNormSpace
for X being set
for f being PartFunc of the carrier of CNS,COMPLEX holds
( f is_Lipschitzian_on X iff ( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) ) );

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

:: deftheorem Def21 defines is_Lipschitzian_on NCFCONT1:def_21_:_
 for CNS being ComplexNormSpace
for X being set
for f being PartFunc of the carrier of CNS,REAL holds
( f is_Lipschitzian_on X iff ( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X holds
abs ((f /. x1) - (f /. x2)) <= r * ||.(x1 - x2).|| ) ) ) );

definition
let RNS be RealNormSpace;
let X be set ;
let f be PartFunc of the carrier of RNS,COMPLEX;
predf is_Lipschitzian_on X means :Def22: :: NCFCONT1:def 22
( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of RNS st x1 in X &amp; x2 in X holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) );
end;

:: deftheorem Def22 defines is_Lipschitzian_on NCFCONT1:def_22_:_
 for RNS being RealNormSpace
for X being set
for f being PartFunc of the carrier of RNS,COMPLEX holds
( f is_Lipschitzian_on X iff ( X c= dom f &amp; ex r being Real st
( 0 < r &amp; ( for x1, x2 being Point of RNS st x1 in X &amp; x2 in X holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) ) );

theorem Th97: :: NCFCONT1:97
for CNS1, CNS2 being ComplexNormSpace
for X, X1 being set
for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X &amp; X1 c= X holds
f is_Lipschitzian_on X1
proofend;

theorem Th98: :: NCFCONT1:98
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X &amp; X1 c= X holds
f is_Lipschitzian_on X1
proofend;

theorem Th99: :: NCFCONT1:99
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X &amp; X1 c= X holds
f is_Lipschitzian_on X1
proofend;

theorem :: NCFCONT1:100
for CNS1, CNS2 being ComplexNormSpace
for X, X1 being set
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X &amp; f2 is_Lipschitzian_on X1 holds
f1 + f2 is_Lipschitzian_on X /\ X1
proofend;

theorem :: NCFCONT1:101
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of CNS,RNS st f1 is_Lipschitzian_on X &amp; f2 is_Lipschitzian_on X1 holds
f1 + f2 is_Lipschitzian_on X /\ X1
proofend;

theorem :: NCFCONT1:102
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of RNS,CNS st f1 is_Lipschitzian_on X &amp; f2 is_Lipschitzian_on X1 holds
f1 + f2 is_Lipschitzian_on X /\ X1
proofend;

theorem :: NCFCONT1:103
for CNS1, CNS2 being ComplexNormSpace
for X, X1 being set
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X &amp; f2 is_Lipschitzian_on X1 holds
f1 - f2 is_Lipschitzian_on X /\ X1
proofend;

theorem :: NCFCONT1:104
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of CNS,RNS st f1 is_Lipschitzian_on X &amp; f2 is_Lipschitzian_on X1 holds
f1 - f2 is_Lipschitzian_on X /\ X1
proofend;

theorem :: NCFCONT1:105
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of RNS,CNS st f1 is_Lipschitzian_on X &amp; f2 is_Lipschitzian_on X1 holds
f1 - f2 is_Lipschitzian_on X /\ X1
proofend;

theorem Th106: :: NCFCONT1:106
for z being Complex
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
z (#) f is_Lipschitzian_on X
proofend;

theorem Th107: :: NCFCONT1:107
for r being Real
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds
r (#) f is_Lipschitzian_on X
proofend;

theorem Th108: :: NCFCONT1:108
for z being Complex
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds
z (#) f is_Lipschitzian_on X
proofend;

theorem :: NCFCONT1:109
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
( - f is_Lipschitzian_on X &amp; ||.f.|| is_Lipschitzian_on X )
proofend;

theorem :: NCFCONT1:110
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds
( - f is_Lipschitzian_on X &amp; ||.f.|| is_Lipschitzian_on X )
proofend;

theorem :: NCFCONT1:111
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds
( - f is_Lipschitzian_on X &amp; ||.f.|| is_Lipschitzian_on X )
proofend;

theorem Th112: :: NCFCONT1:112
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 st X c= dom f &amp; f | X is V20() holds
f is_Lipschitzian_on X
proofend;

theorem Th113: :: NCFCONT1:113
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st X c= dom f &amp; f | X is V20() holds
f is_Lipschitzian_on X
proofend;

theorem Th114: :: NCFCONT1:114
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS st X c= dom f &amp; f | X is V20() holds
f is_Lipschitzian_on X
proofend;

theorem :: NCFCONT1:115
for CNS being ComplexNormSpace
for Y being Subset of CNS holds id Y is_Lipschitzian_on Y
proofend;

theorem Th116: :: NCFCONT1:116
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
f is_continuous_on X
proofend;

theorem Th117: :: NCFCONT1:117
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds
f is_continuous_on X
proofend;

theorem Th118: :: NCFCONT1:118
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds
f is_continuous_on X
proofend;

theorem :: NCFCONT1:119
for CNS being ComplexNormSpace
for X being set
for f being PartFunc of the carrier of CNS,COMPLEX st f is_Lipschitzian_on X holds
f is_continuous_on X
proofend;

theorem Th120: :: NCFCONT1:120
for CNS being ComplexNormSpace
for X being set
for f being PartFunc of the carrier of CNS,REAL st f is_Lipschitzian_on X holds
f is_continuous_on X
proofend;

theorem :: NCFCONT1:121
for RNS being RealNormSpace
for X being set
for f being PartFunc of the carrier of RNS,COMPLEX st f is_Lipschitzian_on X holds
f is_continuous_on X
proofend;

theorem :: NCFCONT1:122
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st ex r being Point of CNS2 st rng f = {r} holds
f is_continuous_on dom f
proofend;

theorem :: NCFCONT1:123
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS st ex r being Point of RNS st rng f = {r} holds
f is_continuous_on dom f
proofend;

theorem :: NCFCONT1:124
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS st ex r being Point of CNS st rng f = {r} holds
f is_continuous_on dom f
proofend;

theorem :: NCFCONT1:125
for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 st X c= dom f &amp; f | X is V20() holds
f is_continuous_on X by Th112, Th116;

theorem :: NCFCONT1:126
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st X c= dom f &amp; f | X is V20() holds
f is_continuous_on X by Th113, Th117;

theorem :: NCFCONT1:127
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS st X c= dom f &amp; f | X is V20() holds
f is_continuous_on X by Th114, Th118;

theorem Th128: :: NCFCONT1:128
for CNS being ComplexNormSpace
for f being PartFunc of CNS,CNS st ( for x0 being Point of CNS st x0 in dom f holds
f /. x0 = x0 ) holds
f is_continuous_on dom f
proofend;

theorem :: NCFCONT1:129
for CNS being ComplexNormSpace
for f being PartFunc of CNS,CNS st f = id (dom f) holds
f is_continuous_on dom f
proofend;

theorem :: NCFCONT1:130
for CNS being ComplexNormSpace
for f being PartFunc of CNS,CNS
for Y being Subset of CNS st Y c= dom f &amp; f | Y = id Y holds
f is_continuous_on Y
proofend;

theorem :: NCFCONT1:131
for CNS being ComplexNormSpace
for X being set
for f being PartFunc of CNS,CNS
for z being Complex
for p being Point of CNS st X c= dom f &amp; ( for x0 being Point of CNS st x0 in X holds
f /. x0 = (z * x0) + p ) holds
f is_continuous_on X
proofend;

theorem Th132: :: NCFCONT1:132
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL st ( for x0 being Point of CNS st x0 in dom f holds
f /. x0 = ||.x0.|| ) holds
f is_continuous_on dom f
proofend;

theorem :: NCFCONT1:133
for CNS being ComplexNormSpace
for X being set
for f being PartFunc of the carrier of CNS,REAL st X c= dom f &amp; ( for x0 being Point of CNS st x0 in X holds
f /. x0 = ||.x0.|| ) holds
f is_continuous_on X
proofend;