:: Continuous Functions on Real and Complex Normed Linear Spaces
::  by Noboru Endou
::
:: Received August 20, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, REAL_1, XCMPLX_0, CLVECT_1, NORMSP_1, NAT_1,
      ARYTM_1, ARYTM_3, COMPLEX1, RELAT_1, FUNCT_1, PARTFUN1, STRUCT_0,
      PRE_TOPC, RCOMP_1, CARD_1, TARSKI, XXREAL_0, SUPINF_2, VALUED_0, SEQ_2,
      ORDINAL2, FCONT_1, FUNCT_2, XBOOLE_0, VALUED_1, CFCONT_1, COMSEQ_1,
      SEQ_1, SEQ_4, NFCONT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      PARTFUN2, FUNCT_2, PRE_TOPC, XREAL_0, ORDINAL1, NUMBERS, XCMPLX_0,
      COMPLEX1, REAL_1, NAT_1, RLVECT_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4,
      VFUNCT_1, COMSEQ_1, CFCONT_1, RCOMP_1, COMSEQ_2, STRUCT_0, VFUNCT_2,
      CLVECT_1, NFCONT_1, XXREAL_0, NORMSP_0, NORMSP_1;
 constructors REAL_1, SEQ_4, RCOMP_1, PARTFUN2, COMSEQ_2, COMSEQ_3, CFCONT_1,
      NFCONT_1, VFUNCT_2, SEQ_2, RELSET_1;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, NAT_1, STRUCT_0,
      VALUED_0, XREAL_0, VFUNCT_1, FUNCT_2, XCMPLX_0;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Continuous Function on Normed Complex Linear Spaces

reserve n,m for Element of NAT;
reserve r,s for Real;
reserve z for Complex;
reserve CNS,CNS1,CNS2 for ComplexNormSpace;
reserve RNS for RealNormSpace;

theorem :: NCFCONT1:1
  for seq be sequence of CNS holds -seq=(-1r)*seq;

definition

  let CNS;
  let x0 be Point of CNS;
  mode Neighbourhood of x0 -> Subset of CNS means
:: NCFCONT1:def 1

    ex g be Real st 0<g &
     {y where y is Point of CNS: ||.y-x0 .|| < g} c= it;
end;

theorem :: NCFCONT1:2
  for x0 be Point of CNS for g be Real st 0 < g holds {y where y is
  Point of CNS: ||.y-x0 .|| < g} is Neighbourhood of x0;

theorem :: NCFCONT1:3
  for x0 be Point of CNS for N being Neighbourhood of x0 holds x0 in N;

definition
  let CNS;
  let X be Subset of CNS;
  attr X is compact means
:: NCFCONT1:def 2

  for s1 be sequence of CNS st rng s1 c= X ex
s2 be sequence of CNS st s2 is subsequence of s1 & s2 is convergent & lim s2 in
  X;
end;

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

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

definition

  let CNS1,CNS2;
  let f be PartFunc of CNS1,CNS2;
  let x0 be Point of CNS1;
  pred f is_continuous_in x0 means
:: NCFCONT1:def 5

  x0 in dom f & for seq be sequence
of CNS1 st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
  convergent & f/.x0 = lim (f/*seq);
end;

definition
  let CNS,RNS;
  let f be PartFunc of CNS,RNS;
  let x0 be Point of CNS;
  pred f is_continuous_in x0 means
:: NCFCONT1:def 6

  x0 in dom f & for seq be sequence
  of CNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
  convergent & f/.x0 = lim (f/*seq);
end;

definition
  let RNS;
  let CNS;
  let f be PartFunc of RNS,CNS;
  let x0 be Point of RNS;
  pred f is_continuous_in x0 means
:: NCFCONT1:def 7

  x0 in dom f & for seq be sequence
  of RNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
  convergent & f/.x0 = lim (f/*seq);
end;

definition
  let CNS;
  let f be PartFunc of the carrier of CNS,COMPLEX;
  let x0 be Point of CNS;
  pred f is_continuous_in x0 means
:: NCFCONT1:def 8

  x0 in dom f & for seq be sequence
  of CNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
  convergent & f/.x0 = lim (f/*seq);
end;

definition
  let CNS;
  let f be PartFunc of the carrier of CNS,REAL;
  let x0 be Point of CNS;
  pred f is_continuous_in x0 means
:: NCFCONT1:def 9

  x0 in dom f & for seq be sequence
  of CNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
  convergent & f/.x0 = lim (f/*seq);
end;

definition
  let RNS;
  let f be PartFunc of the carrier of RNS,COMPLEX;
  let x0 be Point of RNS;
  pred f is_continuous_in x0 means
:: NCFCONT1:def 10

  x0 in dom f & for seq be sequence
  of RNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
  convergent & f/.x0 = lim (f/*seq);
end;

theorem :: NCFCONT1:4
  for n being Nat
  for seq be sequence of CNS1, h be PartFunc of CNS1,CNS2 st rng
  seq c= dom h
   holds seq.n in dom h;

theorem :: NCFCONT1:5
  for n being Nat
  for seq be sequence of CNS, h be PartFunc of CNS,RNS st rng seq
  c= dom h holds seq.n in dom h;

theorem :: NCFCONT1:6
  for n being Nat
  for seq be sequence of RNS, h be PartFunc of RNS,CNS st rng seq
  c= dom h holds seq.n in dom h;

theorem :: NCFCONT1:7
  for seq be sequence of CNS, x be set holds x in rng seq
  iff ex n being Nat st x = seq.n;

theorem :: NCFCONT1:8
  for f be PartFunc of CNS1,CNS2, x0 be Point of CNS1 holds f
  is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s & for x1 be
  Point of CNS1 st x1 in dom f & ||. x1- x0 .|| <s holds ||. f/.x1-f/.x0 .||<r;

theorem :: NCFCONT1:9
  for f be PartFunc of CNS,RNS, x0 be Point of CNS holds f
  is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s & for x1 be
  Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds ||. f/.x1-f/.x0 .||<r;

theorem :: NCFCONT1:10
  for f be PartFunc of RNS,CNS, x0 be Point of RNS holds f
  is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s & for x1 be
  Point of RNS st x1 in dom f & ||. x1- x0 .|| < s holds ||. f/.x1-f/.x0 .||<r;

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

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

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

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

theorem :: NCFCONT1:15
  for f be PartFunc of CNS,RNS,x0 be Point of CNS holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
  being Neighbourhood of x0 st for x1 be Point of CNS st x1 in dom f & x1 in N
  holds f/.x1 in N1;

theorem :: NCFCONT1:16
  for f be PartFunc of RNS,CNS, x0 be Point of RNS holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
  being Neighbourhood of x0 st for x1 be Point of RNS st x1 in dom f & x1 in N
  holds f/.x1 in N1;

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

theorem :: NCFCONT1:18
  for f be PartFunc of CNS,RNS, x0 be Point of CNS holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
  being Neighbourhood of x0 st f.:N c= N1;

theorem :: NCFCONT1:19
  for f be PartFunc of RNS,CNS, x0 be Point of RNS holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
  being Neighbourhood of x0 st f.:N c= N1;

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: NCFCONT1:32
  for f1,f2 be PartFunc of CNS1,CNS2, x0 be Point of CNS1 st f1
is_continuous_in x0 & f2 is_continuous_in x0 holds f1+f2 is_continuous_in x0 &
  f1-f2 is_continuous_in x0;

theorem :: NCFCONT1:33
  for f1,f2 be PartFunc of CNS,RNS, x0 be Point of CNS st f1
is_continuous_in x0 & f2 is_continuous_in x0 holds f1+f2 is_continuous_in x0 &
  f1-f2 is_continuous_in x0;

theorem :: NCFCONT1:34
  for f1,f2 be PartFunc of RNS,CNS, x0 be Point of RNS st f1
is_continuous_in x0 & f2 is_continuous_in x0 holds f1+f2 is_continuous_in x0 &
  f1-f2 is_continuous_in x0;

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

theorem :: NCFCONT1:36
  for f be PartFunc of CNS,RNS, x0 be Point of CNS, r be Real st f
  is_continuous_in x0 holds r(#)f is_continuous_in x0;

theorem :: NCFCONT1:37
  for f be PartFunc of RNS,CNS, x0 be Point of RNS, z be Complex
  st f is_continuous_in x0 holds z(#)f is_continuous_in x0;

theorem :: NCFCONT1:38
  for f be PartFunc of CNS1,CNS2, x0 be Point of CNS1 st f
  is_continuous_in x0 holds ||. f .|| is_continuous_in x0 & -f is_continuous_in
  x0;

theorem :: NCFCONT1:39
  for f be PartFunc of CNS,RNS, x0 be Point of CNS st f is_continuous_in
  x0 holds ||. f .|| is_continuous_in x0 & -f is_continuous_in x0;

theorem :: NCFCONT1:40
  for f be PartFunc of RNS,CNS, x0 be Point of RNS st f is_continuous_in
  x0 holds ||. f .|| is_continuous_in x0 & -f is_continuous_in x0;

definition
  let CNS1,CNS2 be ComplexNormSpace;
  let f be PartFunc of CNS1,CNS2;
  let X be set;
  pred f is_continuous_on X means
:: NCFCONT1:def 11

  X c= dom f & for x0 be Point of CNS1
  st x0 in X holds f|X is_continuous_in x0;
end;

definition
  let CNS be ComplexNormSpace;
  let RNS be RealNormSpace;
  let f be PartFunc of CNS,RNS;
  let X be set;
  pred f is_continuous_on X means
:: NCFCONT1:def 12

  X c= dom f & for x0 be Point of CNS st x0 in X holds f|X is_continuous_in x0;
end;

definition
  let RNS be RealNormSpace;
  let CNS be ComplexNormSpace;
  let g be PartFunc of RNS,CNS;
  let X be set;
  pred g is_continuous_on X means
:: NCFCONT1:def 13

  X c= dom g & for x0 be Point of RNS st x0 in X holds g|X is_continuous_in x0;
end;

definition
  let CNS be ComplexNormSpace;
  let f be PartFunc of the carrier of CNS, COMPLEX;
  let X be set;
  pred f is_continuous_on X means
:: NCFCONT1:def 14

  X c= dom f & for x0 be Point of CNS st x0 in X holds f|X is_continuous_in x0;
end;

definition
  let CNS be ComplexNormSpace;
  let f be PartFunc of the carrier of CNS, REAL;
  let X be set;
  pred f is_continuous_on X means
:: NCFCONT1:def 15

  X c= dom f & for x0 be Point of CNS st x0 in X holds f|X is_continuous_in x0;
end;

definition
  let RNS be RealNormSpace;
  let f be PartFunc of the carrier of RNS, COMPLEX;
  let X be set;
  pred f is_continuous_on X means
:: NCFCONT1:def 16

  X c= dom f & for x0 be Point of RNS st x0 in X holds f|X is_continuous_in x0;
end;

reserve X,X1 for set;

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

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

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

theorem :: NCFCONT1:44
  for f be PartFunc of CNS1,CNS2 holds f is_continuous_on X iff X
c= dom f & for x0 be Point of CNS1, r st x0 in X & 0<r ex s st 0<s & for x1 be
  Point of CNS1 st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0 .|| < r
;

theorem :: NCFCONT1:45
  for f be PartFunc of CNS,RNS holds f is_continuous_on X iff X c=
  dom f & for x0 be Point of CNS, r st x0 in X & 0<r ex s st 0<s & for x1 be
  Point of CNS st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0 .|| < r;

theorem :: NCFCONT1:46
  for f be PartFunc of RNS,CNS holds f is_continuous_on X iff X c=
  dom f & for x0 be Point of RNS, r st x0 in X & 0<r ex s st 0<s & for x1 be
  Point of RNS st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0 .|| < r;

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

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

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

theorem :: NCFCONT1:50
  for f be PartFunc of CNS1,CNS2 holds f is_continuous_on X iff f|X
  is_continuous_on X;

theorem :: NCFCONT1:51
  for f be PartFunc of CNS,RNS holds f is_continuous_on X iff f|X
  is_continuous_on X;

theorem :: NCFCONT1:52
  for f be PartFunc of RNS,CNS holds f is_continuous_on X iff f|X
  is_continuous_on X;

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

theorem :: NCFCONT1:54
  for f be PartFunc of the carrier of CNS,REAL holds (f
  is_continuous_on X iff f|X is_continuous_on X);

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

theorem :: NCFCONT1:56
  for f be PartFunc of CNS1,CNS2 st f is_continuous_on X & X1 c= X
  holds f is_continuous_on X1;

theorem :: NCFCONT1:57
  for f be PartFunc of CNS,RNS st f is_continuous_on X & X1 c= X
  holds f is_continuous_on X1;

theorem :: NCFCONT1:58
  for f be PartFunc of RNS,CNS st f is_continuous_on X & X1 c= X
  holds f is_continuous_on X1;

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

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

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

theorem :: NCFCONT1:62
  for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_continuous_on X & f2
  is_continuous_on X holds f1+f2 is_continuous_on X & f1-f2 is_continuous_on X;

theorem :: NCFCONT1:63
  for f1,f2 be PartFunc of CNS,RNS st f1 is_continuous_on X & f2
  is_continuous_on X holds f1+f2 is_continuous_on X & f1-f2 is_continuous_on X;

theorem :: NCFCONT1:64
  for f1,f2 be PartFunc of RNS,CNS st f1 is_continuous_on X & f2
  is_continuous_on X holds f1+f2 is_continuous_on X & f1-f2 is_continuous_on X;

theorem :: NCFCONT1:65
  for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_continuous_on X & f2
  is_continuous_on X1 holds f1+f2 is_continuous_on X /\ X1 & f1-f2
  is_continuous_on X /\ X1;

theorem :: NCFCONT1:66
  for f1,f2 be PartFunc of CNS,RNS st f1 is_continuous_on X & f2
  is_continuous_on X1 holds f1+f2 is_continuous_on X /\ X1 & f1-f2
  is_continuous_on X /\ X1;

theorem :: NCFCONT1:67
  for f1,f2 be PartFunc of RNS,CNS st f1 is_continuous_on X & f2
  is_continuous_on X1 holds f1+f2 is_continuous_on X /\ X1 & f1-f2
  is_continuous_on X /\ X1;

theorem :: NCFCONT1:68
  for f be PartFunc of CNS1,CNS2 st f is_continuous_on X holds z
  (#)f is_continuous_on X;

theorem :: NCFCONT1:69
  for f be PartFunc of CNS,RNS st f is_continuous_on X holds r(#)f
  is_continuous_on X;

theorem :: NCFCONT1:70
  for f be PartFunc of RNS,CNS st f is_continuous_on X holds z(#)f
  is_continuous_on X;

theorem :: NCFCONT1:71
  for f be PartFunc of CNS1,CNS2 st f is_continuous_on X holds ||.
  f.|| is_continuous_on X & -f is_continuous_on X;

theorem :: NCFCONT1:72
  for f be PartFunc of CNS,RNS st f is_continuous_on X holds ||.f
  .|| is_continuous_on X & -f is_continuous_on X;

theorem :: NCFCONT1:73
  for f be PartFunc of RNS,CNS st f is_continuous_on X holds ||.f
  .|| is_continuous_on X & -f is_continuous_on X;

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

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

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

theorem :: NCFCONT1:77
  for f be PartFunc of CNS1,CNS2 st dom f is compact & f
  is_continuous_on (dom f) holds (rng f) is compact;

theorem :: NCFCONT1:78
  for f be PartFunc of CNS,RNS st dom f is compact & f
  is_continuous_on (dom f) holds (rng f) is compact;

theorem :: NCFCONT1:79
  for f be PartFunc of RNS,CNS st dom f is compact & f
  is_continuous_on (dom f) holds (rng f) is compact;

theorem :: NCFCONT1:80
  for f be PartFunc of the carrier of CNS,COMPLEX st dom f is compact &
  f is_continuous_on (dom f) holds (rng f) is compact;

theorem :: NCFCONT1:81
  for f be PartFunc of the carrier of CNS,REAL st dom f is
  compact & f is_continuous_on (dom f) holds (rng f) is compact;

theorem :: NCFCONT1:82
  for f be PartFunc of the carrier of RNS,COMPLEX st dom f is compact &
  f is_continuous_on (dom f) holds (rng f) is compact;

theorem :: NCFCONT1:83
  for Y be Subset of CNS1, f be PartFunc of CNS1,CNS2 st Y c= dom f & Y
  is compact & f is_continuous_on Y holds (f.:Y) is compact;

theorem :: NCFCONT1:84
  for Y be Subset of CNS, f be PartFunc of CNS,RNS st Y c= dom f & Y is
  compact & f is_continuous_on Y holds (f.:Y) is compact;

theorem :: NCFCONT1:85
  for Y be Subset of RNS, f be PartFunc of RNS,CNS st Y c= dom f & Y is
  compact & f is_continuous_on Y holds (f.:Y) is compact;

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

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

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

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

theorem :: NCFCONT1:90
  for f be PartFunc of CNS1,CNS2 holds (||.f.||)|X = ||.(f|X).||;

theorem :: NCFCONT1:91
  for f be PartFunc of CNS,RNS holds (||.f.||)|X = ||.(f|X).||;

theorem :: NCFCONT1:92
  for f be PartFunc of RNS,CNS holds (||.f.||)|X = ||.(f|X).||;

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

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

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

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

definition
  let CNS1,CNS2 be ComplexNormSpace;
  let X be set;
  let f be PartFunc of CNS1,CNS2;
  pred f is_Lipschitzian_on X means
:: NCFCONT1:def 17

  X c= dom f & ex r st 0 < r & for
x1,x2 be Point of CNS1 st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
  .||;
end;

definition
  let CNS be ComplexNormSpace;
  let RNS be RealNormSpace;
  let X be set;
  let f be PartFunc of CNS,RNS;
  pred f is_Lipschitzian_on X means
:: NCFCONT1:def 18

  X c= dom f & ex r st 0 < r & for
x1,x2 be Point of CNS st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
  .||;
end;

definition
  let RNS be RealNormSpace;
  let CNS be ComplexNormSpace;
  let X be set;
  let f be PartFunc of RNS,CNS;
  pred f is_Lipschitzian_on X means
:: NCFCONT1:def 19

  X c= dom f & ex r st 0 < r & for
x1,x2 be Point of RNS st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
  .||;
end;

definition
  let CNS be ComplexNormSpace;
  let X be set;
  let f be PartFunc of the carrier of CNS,COMPLEX;
  pred f is_Lipschitzian_on X means
:: NCFCONT1:def 20

  X c= dom f & ex r st 0<r & for x1,
x2 be Point of CNS st x1 in X & x2 in X holds |.(f/.x1-f/.x2).|<=r*||.x1-x2.||;
end;

definition
  let CNS be ComplexNormSpace;
  let X be set;
  let f be PartFunc of the carrier of CNS,REAL;
  pred f is_Lipschitzian_on X means
:: NCFCONT1:def 21

  X c= dom f & ex r st 0<r & for x1,
x2 be Point of CNS st x1 in X & x2 in X holds |.f/.x1-f/.x2.|<=r*||.x1-x2.||;
end;

definition
  let RNS be RealNormSpace;
  let X be set;
  let f be PartFunc of the carrier of RNS,COMPLEX;
  pred f is_Lipschitzian_on X means
:: NCFCONT1:def 22

  X c= dom f & ex r st 0<r & for x1,
x2 be Point of RNS st x1 in X & x2 in X holds |.(f/.x1-f/.x2).|<=r*||.x1-x2.||;
end;

theorem :: NCFCONT1:97
  for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X & X1
  c= X holds f is_Lipschitzian_on X1;

theorem :: NCFCONT1:98
  for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X & X1 c=
  X holds f is_Lipschitzian_on X1;

theorem :: NCFCONT1:99
  for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X & X1 c=
  X holds f is_Lipschitzian_on X1;

theorem :: NCFCONT1:100
  for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2
  is_Lipschitzian_on X1 holds f1+f2 is_Lipschitzian_on X /\ X1;

theorem :: NCFCONT1:101
  for f1,f2 be PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2
  is_Lipschitzian_on X1 holds f1+f2 is_Lipschitzian_on X /\ X1;

theorem :: NCFCONT1:102
  for f1,f2 be PartFunc of RNS,CNS st f1 is_Lipschitzian_on X & f2
  is_Lipschitzian_on X1 holds f1+f2 is_Lipschitzian_on X /\ X1;

theorem :: NCFCONT1:103
  for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2
  is_Lipschitzian_on X1 holds f1-f2 is_Lipschitzian_on X /\ X1;

theorem :: NCFCONT1:104
  for f1,f2 be PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2
  is_Lipschitzian_on X1 holds f1-f2 is_Lipschitzian_on X /\ X1;

theorem :: NCFCONT1:105
  for f1,f2 be PartFunc of RNS,CNS st f1 is_Lipschitzian_on X & f2
  is_Lipschitzian_on X1 holds f1-f2 is_Lipschitzian_on X /\ X1;

theorem :: NCFCONT1:106
  for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
  z(#)f is_Lipschitzian_on X;

theorem :: NCFCONT1:107
  for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X holds r
  (#)f is_Lipschitzian_on X;

theorem :: NCFCONT1:108
  for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X holds z
  (#)f is_Lipschitzian_on X;

theorem :: NCFCONT1:109
  for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds -f
  is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X;

theorem :: NCFCONT1:110
  for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X holds -f
  is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X;

theorem :: NCFCONT1:111
  for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X holds -f
  is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X;

theorem :: NCFCONT1:112
  for X be set, f be PartFunc of CNS1,CNS2 st X c= dom f & f|X is
  constant holds f is_Lipschitzian_on X;

theorem :: NCFCONT1:113
  for X be set, f be PartFunc of CNS,RNS st X c= dom f & f|X is
  constant holds f is_Lipschitzian_on X;

theorem :: NCFCONT1:114
  for X be set, f be PartFunc of RNS,CNS st X c= dom f & f|X is
  constant holds f is_Lipschitzian_on X;

theorem :: NCFCONT1:115
  for Y be Subset of CNS holds id Y is_Lipschitzian_on Y;

theorem :: NCFCONT1:116
  for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
  f is_continuous_on X;

theorem :: NCFCONT1:117
  for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X holds f
  is_continuous_on X;

theorem :: NCFCONT1:118
  for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X holds f
  is_continuous_on X;

theorem :: NCFCONT1:119
  for f be PartFunc of the carrier of CNS,COMPLEX st f
  is_Lipschitzian_on X holds f is_continuous_on X;

theorem :: NCFCONT1:120
  for f be PartFunc of the carrier of CNS,REAL st f
  is_Lipschitzian_on X holds f is_continuous_on X;

theorem :: NCFCONT1:121
  for f be PartFunc of the carrier of RNS,COMPLEX st f
  is_Lipschitzian_on X holds f is_continuous_on X;

theorem :: NCFCONT1:122
  for f be PartFunc of CNS1,CNS2 st (ex r be Point of CNS2 st rng f = {r
  }) holds f is_continuous_on dom f;

theorem :: NCFCONT1:123
  for f be PartFunc of CNS,RNS st (ex r be Point of RNS st rng f = {r})
  holds f is_continuous_on (dom f);

theorem :: NCFCONT1:124
  for f be PartFunc of RNS,CNS st (ex r be Point of CNS st rng f = {r})
  holds f is_continuous_on (dom f);

theorem :: NCFCONT1:125
  for f be PartFunc of CNS1,CNS2 st X c= dom f & f|X is constant holds f
  is_continuous_on X;

theorem :: NCFCONT1:126
  for f be PartFunc of CNS,RNS st X c= dom f & f|X is constant holds f
  is_continuous_on X;

theorem :: NCFCONT1:127
  for f be PartFunc of RNS,CNS st X c= dom f & f|X is constant holds f
  is_continuous_on X;

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

theorem :: NCFCONT1:129
  for f be PartFunc of CNS,CNS st f = id dom f holds f is_continuous_on dom f;

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

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

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

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