:: NFCONT_4 semantic presentation

begin


definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let x0 be real number ;
predf is_continuous_in x0 means :Def1: :: NFCONT_4:def 1
 ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_continuous_in x0 );
end;

:: deftheorem Def1 defines is_continuous_in NFCONT_4:def_1_:_
 for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being real number holds
( f is_continuous_in x0 iff ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_continuous_in x0 ) );

theorem Th1: :: NFCONT_4:1
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n) st h = f holds
( f is_continuous_in x0 iff h is_continuous_in x0 )
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n) st h = f holds
( f is_continuous_in x0 iff h is_continuous_in x0 )
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n) st h = f holds
( f is_continuous_in x0 iff h is_continuous_in x0 )
let f be PartFunc of REAL,(REAL n); ::_thesis: for h being PartFunc of REAL,(REAL-NS n) st h = f holds
( f is_continuous_in x0 iff h is_continuous_in x0 )
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( h = f implies ( f is_continuous_in x0 iff h is_continuous_in x0 ) )
assume A1: h = f ; ::_thesis: ( f is_continuous_in x0 iff h is_continuous_in x0 )
hereby  ::_thesis: ( h is_continuous_in x0 implies f is_continuous_in x0 )
assume  f is_continuous_in x0 ; ::_thesis: h is_continuous_in x0
then  ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_continuous_in x0 ) by Def1;
hence  h is_continuous_in x0 by A1; ::_thesis: verum
end;
thus  ( h is_continuous_in x0 implies f is_continuous_in x0 ) by A1, Def1; ::_thesis: verum
end;

theorem Th2: :: NFCONT_4:2
for n being Element of NAT
for X being set
for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
proof
let n be Element of NAT ; ::_thesis: for X being set
for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let X be set ; ::_thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in X & f is_continuous_in x0 implies f | X is_continuous_in x0 )
assume that
A1: x0 in X and
A2: f is_continuous_in x0 ; ::_thesis: f | X is_continuous_in x0
consider g being PartFunc of REAL,(REAL-NS n) such that
A3: ( f = g & g is_continuous_in x0 ) by A2, Def1;
 g | X is_continuous_in x0 by A1, A3, NFCONT_3:6;
hence  f | X is_continuous_in x0 by A3, Def1; ::_thesis: verum
end;

theorem Th3: :: NFCONT_4:3
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
hereby  ::_thesis: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) implies f is_continuous_in x0 )
assume  f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( f = g & g is_continuous_in x0 ) by Def1;
thus  x0 in dom f by A1, NFCONT_3:8; ::_thesis: for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus  for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ::_thesis: verum
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
assume  0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
then consider s being real number  such that
A2: ( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r ) ) by A1, NFCONT_3:8;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus  0 < s by A2; ::_thesis: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r )
assume  ( x1 in dom f & abs (x1 - x0) < s ) ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r
then A3: ||.((g /. x1) - (g /. x0)).|| < r by A1, A2;
 ( g /. x1 = f /. x1 & g /. x0 = f /. x0 ) by A1, REAL_NS1:def_4;
hence  |.((f /. x1) - (f /. x0)).| < r by A3, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
end;
assume A4: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) ; ::_thesis: f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1_being_real_number_st_x1_in_dom_g_&_abs_(x1_-_x0)_<_s_holds_
||.((g_/._x1)_-_(g_/._x0)).||_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r ) )
then consider s being real number  such that
A5: 0 < s and
A6: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r by A4;
take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r ) )
thus  0 < s by A5; ::_thesis: for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds
||.((g /. x1) - (g /. x0)).|| < r
let x1 be real number ; ::_thesis: ( x1 in dom g & abs (x1 - x0) < s implies ||.((g /. x1) - (g /. x0)).|| < r )
assume  ( x1 in dom g & abs (x1 - x0) < s ) ; ::_thesis: ||.((g /. x1) - (g /. x0)).|| < r
then A7: |.((f /. x1) - (f /. x0)).| < r by A6;
 ( g /. x1 = f /. x1 & g /. x0 = f /. x0 ) by REAL_NS1:def_4;
hence  ||.((g /. x1) - (g /. x0)).|| < r by A7, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
then  g is_continuous_in x0 by A4, NFCONT_3:8;
hence  f is_continuous_in x0 by Def1; ::_thesis: verum
end;

theorem Th4: :: NFCONT_4:4
for n being Element of NAT
for r being Real
for z being Element of REAL n
for w being Point of (REAL-NS n) st z = w holds
{  y where y is Element of REAL n : |.(y - z).| < r  }  =  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }
proof
let n be Element of NAT ; ::_thesis: for r being Real
for z being Element of REAL n
for w being Point of (REAL-NS n) st z = w holds
{  y where y is Element of REAL n : |.(y - z).| < r  }  =  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }
let r be Real; ::_thesis: for z being Element of REAL n
for w being Point of (REAL-NS n) st z = w holds
{  y where y is Element of REAL n : |.(y - z).| < r  }  =  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }
let z be Element of REAL n; ::_thesis: for w being Point of (REAL-NS n) st z = w holds
{  y where y is Element of REAL n : |.(y - z).| < r  }  =  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }
let w be Point of (REAL-NS n); ::_thesis: ( z = w implies  {  y where y is Element of REAL n : |.(y - z).| < r  }  =  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }  )
assume A1: z = w ; ::_thesis:  {  y where y is Element of REAL n : |.(y - z).| < r  }  =  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }
set N1 =  {  y where y is Element of REAL n : |.(y - z).| < r  }  ;
set N2 =  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }  ;
A2:  {  y where y is Element of REAL n : |.(y - z).| < r  }  c=  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  y where y is Element of REAL n : |.(y - z).| < r  }  or x in  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }  )
assume  x in  {  y where y is Element of REAL n : |.(y - z).| < r  }  ; ::_thesis: x in  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }
then consider y being Element of REAL n such that
A3: ( x = y & |.(y - z).| < r ) ;
reconsider x1 = x as Element of REAL n by A3;
reconsider x2 = x1 as Point of (REAL-NS n) by REAL_NS1:def_4;
 ||.(x2 - w).|| < r by A1, A3, REAL_NS1:1, REAL_NS1:5;
hence  x in  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }  ; ::_thesis: verum
end;
  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }  c=  {  y where y is Element of REAL n : |.(y - z).| < r  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }  or x in  {  y where y is Element of REAL n : |.(y - z).| < r  }  )
assume  x in  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }  ; ::_thesis: x in  {  y where y is Element of REAL n : |.(y - z).| < r  }
then consider y being Point of (REAL-NS n) such that
A4: ( x = y & ||.(y - w).|| < r ) ;
reconsider x3 = x as Point of (REAL-NS n) by A4;
reconsider x4 = x3 as Element of REAL n by REAL_NS1:def_4;
 |.(x4 - z).| < r by A1, A4, REAL_NS1:1, REAL_NS1:5;
hence  x in  {  y where y is Element of REAL n : |.(y - z).| < r  }  ; ::_thesis: verum
end;
hence   {  y where y is Element of REAL n : |.(y - z).| < r  }  =  {  y where y is Point of (REAL-NS n) : ||.(y - w).|| < r  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let Z be set ;
let f be PartFunc of Z,(REAL n);
deffunc H1( set ) ->  Element of REAL = |.(f /. $1).|;
func|.f.| ->  PartFunc of Z,REAL means :Def2: :: NFCONT_4:def 2
( dom it = dom f & ( for x being set st x in dom it holds
it /. x = |.(f /. x).| ) );
existence
 ex b1 being PartFunc of Z,REAL st
( dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 /. x = |.(f /. x).| ) )
proof
consider g being Function such that
A1: ( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
now__::_thesis:_for_y_being_set_st_y_in_rng_g_holds_
y_in_REAL
let y be set ; ::_thesis: ( y in rng g implies y in REAL )
assume  y in rng g ; ::_thesis: y in REAL
then consider x being set  such that
A2: ( x in dom g & y = g . x ) by FUNCT_1:def_3;
 g . x = H1(x) by A1, A2;
hence  y in REAL by A2; ::_thesis: verum
end;
then  rng g c= REAL by TARSKI:def_3;
then  g in PFuncs (Z,REAL) by A1, PARTFUN1:def_3;
then reconsider g = g as PartFunc of Z,REAL by PARTFUN1:46;
take  g ; ::_thesis: ( dom g = dom f & ( for x being set st x in dom g holds
g /. x = |.(f /. x).| ) )
thus  dom g = dom f by A1; ::_thesis: for x being set st x in dom g holds
g /. x = |.(f /. x).|
let x be set ; ::_thesis: ( x in dom g implies g /. x = |.(f /. x).| )
assume A3: x in dom g ; ::_thesis: g /. x = |.(f /. x).|
then  g . x = H1(x) by A1;
hence  g /. x = |.(f /. x).| by A3, PARTFUN1:def_6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of Z,REAL st dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 /. x = |.(f /. x).| ) & dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 /. x = |.(f /. x).| ) holds
b1 = b2
proof
let g1, g2 be PartFunc of Z,REAL; ::_thesis: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = |.(f /. x).| ) & dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = |.(f /. x).| ) implies g1 = g2 )
assume that
A4: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = H1(x) ) ) and
A5: ( dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = H1(x) ) ) ; ::_thesis: g1 = g2
now__::_thesis:_for_x_being_Element_of_Z_st_x_in_dom_g1_holds_
g1_._x_=_g2_._x
let x be Element of Z; ::_thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A6: x in dom g1 ; ::_thesis: g1 . x = g2 . x
then A7: g1 /. x = |.(f /. x).| by A4;
 g1 /. x = g2 /. x by A5, A7, A4, A6;
then  g1 . x = g2 /. x by A6, PARTFUN1:def_6;
hence  g1 . x = g2 . x by A4, A5, A6, PARTFUN1:def_6; ::_thesis: verum
end;
hence  g1 = g2 by A4, A5, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines |. NFCONT_4:def_2_:_
 for n being Element of NAT
for Z being set
for f being PartFunc of Z,(REAL n)
for b4 being PartFunc of Z,REAL holds
( b4 = |.f.| iff ( dom b4 = dom f & ( for x being set st x in dom b4 holds
b4 /. x = |.(f /. x).| ) ) );

definition
let n be Element of NAT ;
let Z be non empty set ;
let f be PartFunc of Z,(REAL n);
deffunc H1( set ) ->  M13( REAL , REAL n) = - (f /. $1);
defpred S1[ set ] means $1 in dom f;
func - f ->  PartFunc of Z,(REAL n) means :Def3: :: NFCONT_4:def 3
( dom it = dom f & ( for c being set st c in dom it holds
it /. c = - (f /. c) ) );
existence
 ex b1 being PartFunc of Z,(REAL n) st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 /. c = - (f /. c) ) )
proof
consider F being PartFunc of Z,(REAL n) such that
A1: for c being Element of Z holds
( c in dom F iff S1[c] ) and
A2: for c being Element of Z st c in dom F holds
F /. c = H1(c) from PARTFUN2:sch_2();
take  F ; ::_thesis: ( dom F = dom f & ( for c being set st c in dom F holds
F /. c = - (f /. c) ) )
thus  ( dom F = dom f & ( for c being set st c in dom F holds
F /. c = - (f /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of Z,(REAL n) st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 /. c = - (f /. c) ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 /. c = - (f /. c) ) holds
b1 = b2
proof
let g1, g2 be PartFunc of Z,(REAL n); ::_thesis: ( dom g1 = dom f & ( for c being set st c in dom g1 holds
g1 /. c = - (f /. c) ) & dom g2 = dom f & ( for c being set st c in dom g2 holds
g2 /. c = - (f /. c) ) implies g1 = g2 )
assume that
A3: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = - (f /. x) ) ) and
A4: ( dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = - (f /. x) ) ) ; ::_thesis: g1 = g2
now__::_thesis:_for_x_being_Element_of_Z_st_x_in_dom_g1_holds_
g1_._x_=_g2_._x
let x be Element of Z; ::_thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A5: x in dom g1 ; ::_thesis: g1 . x = g2 . x
then A6: g1 /. x = - (f /. x) by A3;
 g1 /. x = g2 /. x by A4, A6, A3, A5;
then  g1 . x = g2 /. x by A5, PARTFUN1:def_6;
hence  g1 . x = g2 . x by A3, A4, A5, PARTFUN1:def_6; ::_thesis: verum
end;
hence  g1 = g2 by A3, A4, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines - NFCONT_4:def_3_:_
 for n being Element of NAT
for Z being non empty set
for f, b4 being PartFunc of Z,(REAL n) holds
( b4 = - f iff ( dom b4 = dom f & ( for c being set st c in dom b4 holds
b4 /. c = - (f /. c) ) ) );

theorem Th5: :: NFCONT_4:5
for n being Element of NAT
for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
proof
let n be Element of NAT ; ::_thesis: for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let W be non empty set ; ::_thesis: for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let f1, f2 be PartFunc of W,(REAL-NS n); ::_thesis: for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let g1, g2 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 + f2 = g1 + g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 + f2 = g1 + g2
A2: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_1;
then A3: dom (f1 + f2) = dom (g1 + g2) by A1, VALUED_2:def_45;
A4: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(f1_+_f2)_holds_
(f1_+_f2)_._x_=_(g1_+_g2)_._x
let x be Element of W; ::_thesis: ( x in dom (f1 + f2) implies (f1 + f2) . x = (g1 + g2) . x )
assume A5: x in dom (f1 + f2) ; ::_thesis: (f1 + f2) . x = (g1 + g2) . x
then A6: ( x in dom g1 & x in dom g2 ) by A2, A1, XBOOLE_0:def_4;
A7: ( f1 /. x = g1 /. x & f2 /. x = g2 /. x ) by A1, REAL_NS1:def_4;
 ( g1 /. x = g1 . x & g2 /. x = g2 . x ) by A6, PARTFUN1:def_6;
then A8: (f1 /. x) + (f2 /. x) = (g1 . x) + (g2 . x) by A7, REAL_NS1:2;
 (f1 + f2) /. x = (f1 /. x) + (f2 /. x) by A5, VFUNCT_1:def_1;
then  (f1 + f2) . x = (f1 /. x) + (f2 /. x) by A5, PARTFUN1:def_6;
hence  (f1 + f2) . x = (g1 + g2) . x by A8, A3, A5, VALUED_2:def_45; ::_thesis: verum
end;
 f1 + f2 is PartFunc of W,(REAL n) by REAL_NS1:def_4;
hence  f1 + f2 = g1 + g2 by A3, A4, PARTFUN1:5; ::_thesis: verum
end;

theorem Th6: :: NFCONT_4:6
for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
proof
let n be Element of NAT ; ::_thesis: for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let f1 be PartFunc of W,(REAL-NS n); ::_thesis: for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let g1 be PartFunc of W,(REAL n); ::_thesis: for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
let a be Real; ::_thesis: ( f1 = g1 implies a (#) f1 = a (#) g1 )
assume A1: f1 = g1 ; ::_thesis: a (#) f1 = a (#) g1
A2: dom (a (#) f1) = dom f1 by VFUNCT_1:def_4;
then A3: dom (a (#) f1) = dom (a (#) g1) by A1, VALUED_2:def_39;
A4: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(a_(#)_f1)_holds_
(a_(#)_f1)_._x_=_(a_(#)_g1)_._x
let x be Element of W; ::_thesis: ( x in dom (a (#) f1) implies (a (#) f1) . x = (a (#) g1) . x )
assume A5: x in dom (a (#) f1) ; ::_thesis: (a (#) f1) . x = (a (#) g1) . x
then A6: g1 . x = g1 /. x by A1, A2, PARTFUN1:def_6;
 f1 /. x = g1 /. x by A1, REAL_NS1:def_4;
then A7: a * (f1 /. x) = a * (g1 /. x) by REAL_NS1:3;
A8: (a (#) f1) /. x = a * (f1 /. x) by A5, VFUNCT_1:def_4;
 (a (#) g1) . x = a (#) (g1 . x) by A3, A5, VALUED_2:def_39;
hence  (a (#) f1) . x = (a (#) g1) . x by A5, A7, A8, A6, PARTFUN1:def_6; ::_thesis: verum
end;
 a (#) f1 is PartFunc of W,(REAL n) by REAL_NS1:def_4;
hence  a (#) f1 = a (#) g1 by A3, A4, PARTFUN1:5; ::_thesis: verum
end;

theorem :: NFCONT_4:7
for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1
proof
let n be Element of NAT ; ::_thesis: for W being non empty set
for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1
let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1
let f1 be PartFunc of W,(REAL n); ::_thesis: (- 1) (#) f1 = - f1
A1: dom ((- 1) (#) f1) = dom f1 by VALUED_2:def_39;
then A2: dom ((- 1) (#) f1) = dom (- f1) by Def3;
now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_((-_1)_(#)_f1)_holds_
((-_1)_(#)_f1)_._x_=_(-_f1)_._x
let x be Element of W; ::_thesis: ( x in dom ((- 1) (#) f1) implies ((- 1) (#) f1) . x = (- f1) . x )
assume A3: x in dom ((- 1) (#) f1) ; ::_thesis: ((- 1) (#) f1) . x = (- f1) . x
A4: f1 . x = f1 /. x by A1, A3, PARTFUN1:def_6;
A5: (- f1) /. x = - (f1 /. x) by A2, A3, Def3;
 (f1 [#] (- 1)) . x = (- 1) (#) (f1 . x) by A3, VALUED_2:def_39;
hence  ((- 1) (#) f1) . x = (- f1) . x by A4, A2, A3, A5, PARTFUN1:def_6; ::_thesis: verum
end;
hence  (- 1) (#) f1 = - f1 by A2, PARTFUN1:5; ::_thesis: verum
end;

theorem Th8: :: NFCONT_4:8
for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
proof
let n be Element of NAT ; ::_thesis: for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
let f1 be PartFunc of W,(REAL-NS n); ::_thesis: for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
let g1 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 implies - f1 = - g1 )
assume A1: f1 = g1 ; ::_thesis: - f1 = - g1
 dom (- f1) = dom f1 by VFUNCT_1:def_5;
then A2: dom (- f1) = dom (- g1) by A1, Def3;
A3: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(-_f1)_holds_
(-_f1)_._x_=_(-_g1)_._x
let x be Element of W; ::_thesis: ( x in dom (- f1) implies (- f1) . x = (- g1) . x )
assume A4: x in dom (- f1) ; ::_thesis: (- f1) . x = (- g1) . x
 f1 /. x = g1 /. x by A1, REAL_NS1:def_4;
then A5: - (f1 /. x) = - (g1 /. x) by REAL_NS1:4;
A6: (- f1) /. x = - (f1 /. x) by A4, VFUNCT_1:def_5;
 (- g1) /. x = - (g1 /. x) by A2, A4, Def3;
then  (- f1) . x = (- g1) /. x by A4, A5, A6, PARTFUN1:def_6;
hence  (- f1) . x = (- g1) . x by A2, A4, PARTFUN1:def_6; ::_thesis: verum
end;
 - f1 is PartFunc of W,(REAL n) by REAL_NS1:def_4;
hence  - f1 = - g1 by A2, A3, PARTFUN1:5; ::_thesis: verum
end;

theorem Th9: :: NFCONT_4:9
for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
proof
let n be Element of NAT ; ::_thesis: for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
let f1 be PartFunc of W,(REAL-NS n); ::_thesis: for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
let g1 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 implies ||.f1.|| = |.g1.| )
assume A1: f1 = g1 ; ::_thesis: ||.f1.|| = |.g1.|
 dom ||.f1.|| = dom f1 by NORMSP_0:def_3;
then A2: dom ||.f1.|| = dom |.g1.| by A1, Def2;
now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_||.f1.||_holds_
||.f1.||_._x_=_|.g1.|_._x
let x be Element of W; ::_thesis: ( x in dom ||.f1.|| implies ||.f1.|| . x = |.g1.| . x )
assume A3: x in dom ||.f1.|| ; ::_thesis: ||.f1.|| . x = |.g1.| . x
A4: f1 /. x = g1 /. x by A1, REAL_NS1:def_4;
set y1 = g1 /. x;
A5: ||.(f1 /. x).|| = |.(g1 /. x).| by A4, REAL_NS1:1;
A6: ||.f1.|| . x = ||.(f1 /. x).|| by A3, NORMSP_0:def_3;
 |.g1.| /. x = |.(g1 /. x).| by A2, A3, Def2;
hence  ||.f1.|| . x = |.g1.| . x by A2, A3, A5, A6, PARTFUN1:def_6; ::_thesis: verum
end;
hence  ||.f1.|| = |.g1.| by A2, PARTFUN1:5; ::_thesis: verum
end;

theorem Th10: :: NFCONT_4:10
for n being Element of NAT
for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
proof
let n be Element of NAT ; ::_thesis: for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let W be non empty set ; ::_thesis: for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let f1, f2 be PartFunc of W,(REAL-NS n); ::_thesis: for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let g1, g2 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 - f2 = g1 - g2
A2: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_2;
then A3: dom (f1 - f2) = dom (g1 - g2) by A1, VALUED_2:def_46;
A4: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_._x_=_(g1_-_g2)_._x
let x be Element of W; ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (g1 - g2) . x )
assume A5: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) . x = (g1 - g2) . x
A6: ( f1 /. x = g1 /. x & f2 /. x = g2 /. x ) by A1, REAL_NS1:def_4;
 ( x in dom f1 & x in dom f2 ) by A5, A2, XBOOLE_0:def_4;
then  ( g1 . x = g1 /. x & g2 /. x = g2 . x ) by A1, PARTFUN1:def_6;
then A7: (f1 /. x) - (f2 /. x) = (g1 . x) - (g2 . x) by A6, REAL_NS1:5;
A8: (f1 - f2) /. x = (f1 /. x) - (f2 /. x) by A5, VFUNCT_1:def_2;
 (f1 - f2) /. x = (f1 - f2) . x by A5, PARTFUN1:def_6;
hence  (f1 - f2) . x = (g1 - g2) . x by A7, A8, A3, A5, VALUED_2:def_46; ::_thesis: verum
end;
 f1 - f2 is PartFunc of W,(REAL n) by REAL_NS1:def_4;
hence  f1 - f2 = g1 - g2 by A3, A4, PARTFUN1:5; ::_thesis: verum
end;

theorem :: NFCONT_4:11
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )
thus  ( f is_continuous_in x0 implies ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) ) ::_thesis: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) implies f is_continuous_in x0 )
proof
assume  f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( f = g & g is_continuous_in x0 ) by Def1;
thus  x0 in dom f by A1, NFCONT_3:9; ::_thesis: for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1
let N01 be Subset of (REAL n); ::_thesis: ( ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N01 ) implies ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N01 )
assume A2: ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N01 ) ; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N01
consider r being Real such that
A3: 0 < r and
A4:  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  = N01 by A2;
 f /. x0 = g /. x0 by A1, REAL_NS1:def_4;
then A5:  {  p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r  }  = N01 by A4, Th4;
  {  p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r  }  is Neighbourhood of g /. x0 by A3, NFCONT_1:3;
then consider N being Neighbourhood of x0 such that
A6: for x1 being real number st x1 in dom g & x1 in N holds
g /. x1 in N01 by A5, A1, NFCONT_3:9;
take  N ; ::_thesis: for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N01
let x1 be real number ; ::_thesis: ( x1 in dom f & x1 in N implies f /. x1 in N01 )
assume  ( x1 in dom f & x1 in N ) ; ::_thesis: f /. x1 in N01
then  g /. x1 in N01 by A1, A6;
hence  f /. x1 in N01 by A1, REAL_NS1:def_4; ::_thesis: verum
end;
assume A7: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) ; ::_thesis: f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_N1_being_Neighbourhood_of_g_/._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x1_being_real_number_st_x1_in_dom_g_&_x1_in_N_holds_
g_/._x1_in_N1
let N1 be Neighbourhood of g /. x0; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom g & x1 in N holds
g /. x1 in N1
consider r being Real such that
A8: 0 < r and
A9:  {  p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r  }  c= N1 by NFCONT_1:def_1;
set N01 =  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  ;
 f /. x0 = g /. x0 by REAL_NS1:def_4;
then A10:  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  =  {  p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r  }  by Th4;
now__::_thesis:_for_x_being_set_st_x_in__{__p_where_p_is_Element_of_REAL_n_:_|.(p_-_(f_/._x0)).|_<_r__}__holds_
x_in_REAL_n
let x be set ; ::_thesis: ( x in  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  implies x in REAL n )
assume  x in  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  ; ::_thesis: x in REAL n
then  ex p being Element of REAL n st
( p = x & |.(p - (f /. x0)).| < r ) ;
hence  x in REAL n ; ::_thesis: verum
end;
then   {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  is Subset of (REAL n) by TARSKI:def_3;
then consider N being Neighbourhood of x0 such that
A11: for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  by A7, A8;
take N = N; ::_thesis: for x1 being real number st x1 in dom g & x1 in N holds
g /. x1 in N1
let x1 be real number ; ::_thesis: ( x1 in dom g & x1 in N implies g /. x1 in N1 )
assume  ( x1 in dom g & x1 in N ) ; ::_thesis: g /. x1 in N1
then  f /. x1 in  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  by A11;
then  g /. x1 in  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  by REAL_NS1:def_4;
hence  g /. x1 in N1 by A9, A10; ::_thesis: verum
end;
then  g is_continuous_in x0 by A7, NFCONT_3:9;
hence  f is_continuous_in x0 by Def1; ::_thesis: verum
end;

theorem :: NFCONT_4:12
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
hereby  ::_thesis: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1 ) implies f is_continuous_in x0 )
assume  f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1 ) )
then A1: g is_continuous_in x0 by Th1;
hence  x0 in dom f by NFCONT_3:10; ::_thesis: for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1
thus  for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1 ::_thesis: verum
proof
let N1 be Subset of (REAL n); ::_thesis: ( ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) implies ex N being Neighbourhood of x0 st f .: N c= N1 )
given r being Real such that A2: ( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) ; ::_thesis: ex N being Neighbourhood of x0 st f .: N c= N1
 f /. x0 = g /. x0 by REAL_NS1:def_4;
then A3:  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  =  {  p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r  }  by Th4;
 N1 is Neighbourhood of g /. x0 by A2, A3, NFCONT_1:3;
then consider N being Neighbourhood of x0 such that
A4: g .: N c= N1 by A1, NFCONT_3:10;
take  N ; ::_thesis: f .: N c= N1
thus  f .: N c= N1 by A4; ::_thesis: verum
end;
end;
assume A5: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ; ::_thesis: f is_continuous_in x0
now__::_thesis:_for_N1_being_Neighbourhood_of_g_/._x0_ex_N_being_Neighbourhood_of_x0_st_g_.:_N_c=_N1
let N1 be Neighbourhood of g /. x0; ::_thesis: ex N being Neighbourhood of x0 st g .: N c= N1
consider r being Real such that
A6: 0 < r and
A7:  {  p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r  }  c= N1 by NFCONT_1:def_1;
set N01 =  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  ;
 f /. x0 = g /. x0 by REAL_NS1:def_4;
then A8:  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  =  {  p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r  }  by Th4;
now__::_thesis:_for_x_being_set_st_x_in__{__p_where_p_is_Element_of_REAL_n_:_|.(p_-_(f_/._x0)).|_<_r__}__holds_
x_in_REAL_n
let x be set ; ::_thesis: ( x in  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  implies x in REAL n )
assume  x in  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  ; ::_thesis: x in REAL n
then  ex p being Element of REAL n st
( p = x & |.(p - (f /. x0)).| < r ) ;
hence  x in REAL n ; ::_thesis: verum
end;
then   {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  is Subset of (REAL n) by TARSKI:def_3;
then consider N being Neighbourhood of x0 such that
A9: f .: N c=  {  p where p is Element of REAL n : |.(p - (f /. x0)).| < r  }  by A5, A6;
take N = N; ::_thesis: g .: N c= N1
thus  g .: N c= N1 by A7, A8, A9, XBOOLE_1:1; ::_thesis: verum
end;
then  g is_continuous_in x0 by A5, NFCONT_3:10;
hence  f is_continuous_in x0 by Th1; ::_thesis: verum
end;

theorem :: NFCONT_4:13
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: ( ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} implies f is_continuous_in x0 )
given N being Neighbourhood of x0 such that A1: (dom f) /\ N = {x0} ; ::_thesis: f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g is_continuous_in x0 by A1, NFCONT_3:11;
hence  f is_continuous_in x0 by Th1; ::_thesis: verum
end;

theorem :: NFCONT_4:14
for n being Element of NAT
for x0 being real number
for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 + f2 is_continuous_in x0
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 + f2 is_continuous_in x0
let x0 be real number ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 + f2 is_continuous_in x0
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies f1 + f2 is_continuous_in x0 )
assume A1: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 ) ; ::_thesis: f1 + f2 is_continuous_in x0
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 is_continuous_in x0 by A1, Th1;
 g2 is_continuous_in x0 by A1, Th1;
then A3: ( g1 + g2 is_continuous_in x0 & g1 - g2 is_continuous_in x0 ) by A1, A2, NFCONT_3:12;
 g1 + g2 = f1 + f2 by Th5;
hence  f1 + f2 is_continuous_in x0 by A3, Th1; ::_thesis: verum
end;

theorem :: NFCONT_4:15
for n being Element of NAT
for x0 being real number
for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 - f2 is_continuous_in x0
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 - f2 is_continuous_in x0
let x0 be real number ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 - f2 is_continuous_in x0
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies f1 - f2 is_continuous_in x0 )
assume A1: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 ) ; ::_thesis: f1 - f2 is_continuous_in x0
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 is_continuous_in x0 by A1, Th1;
 g2 is_continuous_in x0 by A1, Th1;
then A3: ( g1 + g2 is_continuous_in x0 & g1 - g2 is_continuous_in x0 ) by A1, A2, NFCONT_3:12;
 g1 - g2 = f1 - f2 by Th10;
hence  f1 - f2 is_continuous_in x0 by A3, Th1; ::_thesis: verum
end;

theorem :: NFCONT_4:16
for n being Element of NAT
for r being Real
for x0 being real number
for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
proof
let n be Element of NAT ; ::_thesis: for r being Real
for x0 being real number
for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let r be Real; ::_thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_continuous_in x0 implies r (#) f is_continuous_in x0 )
assume A1: f is_continuous_in x0 ; ::_thesis: r (#) f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g is_continuous_in x0 by A1, Th1;
then A2: r (#) g is_continuous_in x0 by NFCONT_3:13;
 r (#) g = r (#) f by Th6;
hence  r (#) f is_continuous_in x0 by A2, Th1; ::_thesis: verum
end;

theorem :: NFCONT_4:17
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
|.f.| is_continuous_in x0
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
|.f.| is_continuous_in x0
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
|.f.| is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in dom f & f is_continuous_in x0 implies |.f.| is_continuous_in x0 )
assume A1: ( x0 in dom f & f is_continuous_in x0 ) ; ::_thesis: |.f.| is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g is_continuous_in x0 by A1, Th1;
then  ||.g.|| is_continuous_in x0 by A1, NFCONT_3:14;
hence  |.f.| is_continuous_in x0 by Th9; ::_thesis: verum
end;

theorem :: NFCONT_4:18
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
- f is_continuous_in x0
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
- f is_continuous_in x0
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
- f is_continuous_in x0
let f be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in dom f & f is_continuous_in x0 implies - f is_continuous_in x0 )
assume A1: ( x0 in dom f & f is_continuous_in x0 ) ; ::_thesis: - f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g is_continuous_in x0 by A1, Th1;
then A2: - g is_continuous_in x0 by A1, NFCONT_3:14;
 - g = - f by Th8;
hence  - f is_continuous_in x0 by A2, Th1; ::_thesis: verum
end;

theorem :: NFCONT_4:19
for n being Element of NAT
for x0 being real number
for S being RealNormSpace
for z being Point of (REAL-NS n)
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds
f2 * f1 is_continuous_in x0
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for S being RealNormSpace
for z being Point of (REAL-NS n)
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds
f2 * f1 is_continuous_in x0
let x0 be real number ; ::_thesis: for S being RealNormSpace
for z being Point of (REAL-NS n)
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds
f2 * f1 is_continuous_in x0
let S be RealNormSpace; ::_thesis: for z being Point of (REAL-NS n)
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds
f2 * f1 is_continuous_in x0
let z be Point of (REAL-NS n); ::_thesis: for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds
f2 * f1 is_continuous_in x0
let f1 be PartFunc of REAL,(REAL n); ::_thesis: for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds
f2 * f1 is_continuous_in x0
let f2 be PartFunc of (REAL-NS n),S; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z implies f2 * f1 is_continuous_in x0 )
assume A1: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z ) ; ::_thesis: f2 * f1 is_continuous_in x0
reconsider g1 = f1 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 is_continuous_in x0 by A1, Th1;
 f1 /. x0 = g1 /. x0 by REAL_NS1:def_4;
hence  f2 * f1 is_continuous_in x0 by A2, A1, NFCONT_3:15; ::_thesis: verum
end;

theorem Th20: :: NFCONT_4:20
for x0 being real number
for S being RealNormSpace
for f1 being PartFunc of REAL,S
for f2 being PartFunc of S,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
proof
let x0 be real number ; ::_thesis: for S being RealNormSpace
for f1 being PartFunc of REAL,S
for f2 being PartFunc of S,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let S be RealNormSpace; ::_thesis: for f1 being PartFunc of REAL,S
for f2 being PartFunc of S,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f1 be PartFunc of REAL,S; ::_thesis: for f2 being PartFunc of S,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f2 be PartFunc of S,REAL; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 )
assume A1: x0 in dom (f2 * f1) ; ::_thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 /. x0 or f2 * f1 is_continuous_in x0 )
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1 /. x0 ; ::_thesis: f2 * f1 is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( not rng s1 c= dom (f2 * f1) or not s1 is convergent or not lim s1 = x0 or ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) ) )
assume that
A4: rng s1 c= dom (f2 * f1) and
A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) )
A6: dom (f2 * f1) c= dom f1 by RELAT_1:25;
A7: rng (f1 /* s1) c= dom f2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f1 /* s1) or x in dom f2 )
assume  x in rng (f1 /* s1) ; ::_thesis: x in dom f2
then consider n being Element of NAT  such that
A8: x = (f1 /* s1) . n by FUNCT_2:113;
 s1 . n in rng s1 by VALUED_0:28;
then  f1 . (s1 . n) in dom f2 by A4, FUNCT_1:11;
hence  x in dom f2 by A4, A6, A8, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum
end;
A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_((f2_*_f1)_/*_s1)_._n_=_(f2_/*_(f1_/*_s1))_._n
let n be Element of NAT ; ::_thesis: ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n
 s1 . n in rng s1 by VALUED_0:28;
then A10: s1 . n in dom f1 by A4, FUNCT_1:11;
thus ((f2 * f1) /* s1) . n = (f2 * f1) . (s1 . n) by A4, FUNCT_2:108
.= f2 . (f1 . (s1 . n)) by A10, FUNCT_1:13
.= f2 . ((f1 /* s1) . n) by A4, A6, FUNCT_2:108, XBOOLE_1:1
.= (f2 /* (f1 /* s1)) . n by A7, FUNCT_2:108 ; ::_thesis: verum
end;
then A11: f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:63;
 rng s1 c= dom f1 by A4, A6, XBOOLE_1:1;
then A12: ( f1 /* s1 is convergent & f1 /. x0 = lim (f1 /* s1) ) by A2, A5, NFCONT_3:def_1;
hence  (f2 * f1) /* s1 is convergent by A3, A7, A11, NFCONT_1:def_6; ::_thesis: (f2 * f1) . x0 = lim ((f2 * f1) /* s1)
thus (f2 * f1) . x0 = (f2 * f1) /. x0 by A1, PARTFUN1:def_6
.= f2 /. (f1 /. x0) by A1, PARTFUN2:3
.= lim (f2 /* (f1 /* s1)) by A12, A3, A7, NFCONT_1:def_6
.= lim ((f2 * f1) /* s1) by A9, FUNCT_2:63 ; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x0 be Element of REAL n;
predf is_continuous_in x0 means :Def4: :: NFCONT_4:def 4
 ex y0 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st
( x0 = y0 & f = g & g is_continuous_in y0 );
end;

:: deftheorem Def4 defines is_continuous_in NFCONT_4:def_4_:_
 for n being Element of NAT
for f being PartFunc of (REAL n),REAL
for x0 being Element of REAL n holds
( f is_continuous_in x0 iff ex y0 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st
( x0 = y0 & f = g & g is_continuous_in y0 ) );

theorem Th21: :: NFCONT_4:21
for n being Element of NAT
for f being PartFunc of (REAL n),REAL
for h being PartFunc of (REAL-NS n),REAL
for x0 being Element of REAL n
for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of (REAL n),REAL
for h being PartFunc of (REAL-NS n),REAL
for x0 being Element of REAL n
for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
let f be PartFunc of (REAL n),REAL; ::_thesis: for h being PartFunc of (REAL-NS n),REAL
for x0 being Element of REAL n
for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
let h be PartFunc of (REAL-NS n),REAL; ::_thesis: for x0 being Element of REAL n
for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
let x0 be Element of REAL n; ::_thesis: for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
let y0 be Point of (REAL-NS n); ::_thesis: ( f = h & x0 = y0 implies ( f is_continuous_in x0 iff h is_continuous_in y0 ) )
assume A1: ( f = h & x0 = y0 ) ; ::_thesis: ( f is_continuous_in x0 iff h is_continuous_in y0 )
hereby  ::_thesis: ( h is_continuous_in y0 implies f is_continuous_in x0 )
assume  f is_continuous_in x0 ; ::_thesis: h is_continuous_in y0
then  ex y1 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st
( x0 = y1 & f = g & g is_continuous_in y1 ) by Def4;
hence  h is_continuous_in y0 by A1; ::_thesis: verum
end;
thus  ( h is_continuous_in y0 implies f is_continuous_in x0 ) by A1, Def4; ::_thesis: verum
end;

theorem Th22: :: NFCONT_4:22
for n being Element of NAT
for x0 being real number
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL n),REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
proof
let n be Element of NAT ; ::_thesis: for x0 being real number
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL n),REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let x0 be real number ; ::_thesis: for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL n),REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f1 be PartFunc of REAL,(REAL n); ::_thesis: for f2 being PartFunc of (REAL n),REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f2 be PartFunc of (REAL n),REAL; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 )
assume A1: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 ) ; ::_thesis: f2 * f1 is_continuous_in x0
reconsider g1 = f1 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
reconsider g2 = f2 as PartFunc of (REAL-NS n),REAL by REAL_NS1:def_4;
A2: g1 is_continuous_in x0 by A1, Th1;
 f1 /. x0 = g1 /. x0 by REAL_NS1:def_4;
then  g2 is_continuous_in g1 /. x0 by A1, Th21;
hence  f2 * f1 is_continuous_in x0 by A2, A1, Th20; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attrf is continuous  means :Def5: :: NFCONT_4:def 5
 for x0 being real number st x0 in dom f holds
f is_continuous_in x0;
end;

:: deftheorem Def5 defines continuous NFCONT_4:def_5_:_
 for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is continuous iff for x0 being real number st x0 in dom f holds
f is_continuous_in x0 );

theorem Th23: :: NFCONT_4:23
for n being Element of NAT
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of REAL,(REAL n) st g = f holds
( g is continuous iff f is continuous )
proof
let n be Element of NAT ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of REAL,(REAL n) st g = f holds
( g is continuous iff f is continuous )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of REAL,(REAL n) st g = f holds
( g is continuous iff f is continuous )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( g = f implies ( g is continuous iff f is continuous ) )
assume A1: g = f ; ::_thesis: ( g is continuous iff f is continuous )
hereby  ::_thesis: ( f is continuous implies g is continuous )
assume A2: g is continuous ; ::_thesis: f is continuous
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_f_holds_
f_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom f implies f is_continuous_in x0 )
assume  x0 in dom f ; ::_thesis: f is_continuous_in x0
then  g is_continuous_in x0 by A2, A1, NFCONT_3:def_2;
hence  f is_continuous_in x0 by A1, Th1; ::_thesis: verum
end;
hence  f is continuous by Def5; ::_thesis: verum
end;
assume A3: f is continuous ; ::_thesis: g is continuous
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_g_holds_
g_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom g implies g is_continuous_in x0 )
assume  x0 in dom g ; ::_thesis: g is_continuous_in x0
then  f is_continuous_in x0 by A3, A1, Def5;
hence  g is_continuous_in x0 by A1, Th1; ::_thesis: verum
end;
hence  g is continuous by NFCONT_3:def_2; ::_thesis: verum
end;

theorem Th24: :: NFCONT_4:24
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n) st X c= dom f holds
( f | X is continuous iff for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
proof
let n be Element of NAT ; ::_thesis: for X being set
for f being PartFunc of REAL,(REAL n) st X c= dom f holds
( f | X is continuous iff for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f holds
( f | X is continuous iff for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f implies ( f | X is continuous iff for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) )
assume A1: X c= dom f ; ::_thesis: ( f | X is continuous iff for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
thus  ( f | X is continuous implies for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ::_thesis: ( ( for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) implies f | X is continuous )
proof
assume A2: f | X is continuous ; ::_thesis: for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
let x0 be real number ; ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
 x0 in dom (f | X) by A1, A3, RELAT_1:62;
then  f | X is_continuous_in x0 by A2, Def5;
then consider s being real number  such that
A5: 0 < s and
A6: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A4, Th3;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus  0 < s by A5; ::_thesis: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be real number ; ::_thesis: ( x1 in X & abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r )
assume that
A7: x1 in X and
A8: abs (x1 - x0) < s ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r
A9: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
then |.((f /. x1) - (f /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A7, PARTFUN2:15
.= |.(((f | X) /. x1) - ((f | X) /. x0)).| by A3, A9, PARTFUN2:15 ;
hence  |.((f /. x1) - (f /. x0)).| < r by A6, A9, A7, A8; ::_thesis: verum
end;
assume A10: for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ; ::_thesis: f | X is continuous
A11: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A12: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
A13: x0 in X by A12, RELAT_1:57;
 for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) )
assume  0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
then consider s being real number  such that
A14: 0 < s and
A15: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r by A10, A13;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
thus  0 < s by A14; ::_thesis: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r
let x1 be real number ; ::_thesis: ( x1 in dom (f | X) & abs (x1 - x0) < s implies |.(((f | X) /. x1) - ((f | X) /. x0)).| < r )
assume that
A16: x1 in dom (f | X) and
A17: abs (x1 - x0) < s ; ::_thesis: |.(((f | X) /. x1) - ((f | X) /. x0)).| < r
|.(((f | X) /. x1) - ((f | X) /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A12, PARTFUN2:15
.= |.((f /. x1) - (f /. x0)).| by A16, PARTFUN2:15 ;
hence  |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A11, A15, A16, A17; ::_thesis: verum
end;
hence  f | X is_continuous_in x0 by Th3, A12; ::_thesis: verum
end;
hence  f | X is continuous by Def5; ::_thesis: verum
end;

registration
let n be Element of NAT ;
cluster Function-like constant  ->  continuous for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is constant holds
b1 is continuous
proof
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is constant implies f is continuous )
assume A1: f is constant ; ::_thesis: f is continuous
now__::_thesis:_for_x0_being_real_number_
for_r_being_Real_st_x0_in_dom_f_&_0_<_r_holds_
ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1_being_real_number_st_x1_in_dom_f_&_abs_(x1_-_x0)_<_s_holds_
|.((f_/._x1)_-_(f_/._x0)).|_<_r_)_)
reconsider s = 1 as real number ;
let x0 be real number ; ::_thesis: for r being Real st x0 in dom f & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
let r be Real; ::_thesis: ( x0 in dom f & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
assume that
A2: x0 in dom f and
A3: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus  0 < s ; ::_thesis: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r )
assume A4: x1 in dom f ; ::_thesis: ( abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r )
assume  abs (x1 - x0) < s ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r
f /. x1 = f . x1 by A4, PARTFUN1:def_6
.= f . x0 by A1, A2, A4, FUNCT_1:def_10
.= f /. x0 by A2, PARTFUN1:def_6 ;
hence  |.((f /. x1) - (f /. x0)).| < r by A3; ::_thesis: verum
end;
then  f | (dom f) is continuous by Th24;
hence  f is continuous by RELAT_1:69; ::_thesis: verum
end;
end;

registration
let n be Element of NAT ;
cluster Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() continuous for Element of bool [:REAL,(REAL n):];
existence
 ex b1 being PartFunc of REAL,(REAL n) st b1 is continuous
proof
take f = the constant PartFunc of REAL,(REAL n); ::_thesis: f is continuous
thus  f is continuous ; ::_thesis: verum
end;
end;

registration
let n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let X be set ;
clusterf | X ->  continuous for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous
proof
 for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A1: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then  x0 in dom f by RELAT_1:57;
then A2: f is_continuous_in x0 by Def5;
 x0 in X by A1, RELAT_1:57;
hence  f | X is_continuous_in x0 by A2, Th2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous by Def5; ::_thesis: verum
end;
end;

theorem :: NFCONT_4:25
for n being Element of NAT
for X, X1 being set
for f being PartFunc of REAL,(REAL n) st f | X is continuous & X1 c= X holds
f | X1 is continuous
proof
let n be Element of NAT ; ::_thesis: for X, X1 being set
for f being PartFunc of REAL,(REAL n) st f | X is continuous & X1 c= X holds
f | X1 is continuous
let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is continuous & X1 c= X holds
f | X1 is continuous
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is continuous & X1 c= X implies f | X1 is continuous )
assume A1: f | X is continuous ; ::_thesis: ( not X1 c= X or f | X1 is continuous )
assume  X1 c= X ; ::_thesis: f | X1 is continuous
then  f | X1 = (f | X) | X1 by RELAT_1:74;
hence  f | X1 is continuous by A1; ::_thesis: verum
end;

registration
let n be Element of NAT ;
cluster empty Function-like  ->  continuous for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is empty holds
b1 is continuous ;
end;

registration
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let X be trivial set ;
clusterf | X ->  continuous for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g | X is continuous PartFunc of REAL,(REAL-NS n) ;
hence  for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous by Th23; ::_thesis: verum
end;
end;

registration
let n be Element of NAT ;
let f1, f2 be continuous PartFunc of REAL,(REAL n);
clusterf1 + f2 ->  continuous for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is continuous
proof
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A1: ( g1 is continuous & g2 is continuous ) by Th23;
 g1 + g2 = f1 + f2 by Th5;
hence  for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is continuous by A1, Th23; ::_thesis: verum
end;
end;

theorem :: NFCONT_4:26
for n being Element of NAT
for X being set
for f1, f2 being PartFunc of REAL,(REAL n) st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
proof
let n be Element of NAT ; ::_thesis: for X being set
for f1, f2 being PartFunc of REAL,(REAL n) st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
let X be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous implies ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) )
assume A1: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous ) ; ::_thesis: ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 | X is continuous by A1, Th23;
 g2 | X is continuous by A1, Th23;
then A3: ( (g1 + g2) | X is continuous & (g1 - g2) | X is continuous ) by A1, A2, NFCONT_3:19;
A4: g1 + g2 = f1 + f2 by Th5;
 g1 - g2 = f1 - f2 by Th10;
hence  ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) by A3, A4, Th23; ::_thesis: verum
end;

theorem :: NFCONT_4:27
for n being Element of NAT
for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds
( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
proof
let n be Element of NAT ; ::_thesis: for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds
( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds
( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous implies ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) )
assume A1: ( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous ) ; ::_thesis: ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: g1 | X is continuous by A1, Th23;
 g2 | X1 is continuous by A1, Th23;
then A3: ( (g1 + g2) | (X /\ X1) is continuous & (g1 - g2) | (X /\ X1) is continuous ) by A1, A2, NFCONT_3:20;
A4: g1 + g2 = f1 + f2 by Th5;
 g1 - g2 = f1 - f2 by Th10;
hence  ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) by A3, A4, Th23; ::_thesis: verum
end;

registration
let n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let r be Real;
clusterr (#) f ->  continuous for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = r (#) f holds
b1 is continuous
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A1: g is continuous by Th23;
 r (#) g = r (#) f by Th6;
hence  for b1 being PartFunc of REAL,(REAL n) st b1 = r (#) f holds
b1 is continuous by A1, Th23; ::_thesis: verum
end;
end;

theorem :: NFCONT_4:28
for n being Element of NAT
for X being set
for r being Real
for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
proof
let n be Element of NAT ; ::_thesis: for X being set
for r being Real
for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let X be set ; ::_thesis: for r being Real
for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let r be Real; ::_thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let f be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous )
assume A1: ( X c= dom f & f | X is continuous ) ; ::_thesis: (r (#) f) | X is continuous
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g | X is continuous PartFunc of REAL,(REAL-NS n) by A1, Th23;
then A2: (r (#) g) | X is continuous by A1, NFCONT_3:21;
 r (#) g = r (#) f by Th6;
hence  (r (#) f) | X is continuous by A2, Th23; ::_thesis: verum
end;

theorem :: NFCONT_4:29
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
( |.f.| | X is continuous & (- f) | X is continuous )
proof
let n be Element of NAT ; ::_thesis: for X being set
for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
( |.f.| | X is continuous & (- f) | X is continuous )
let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
( |.f.| | X is continuous & (- f) | X is continuous )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f & f | X is continuous implies ( |.f.| | X is continuous & (- f) | X is continuous ) )
assume A1: ( X c= dom f & f | X is continuous ) ; ::_thesis: ( |.f.| | X is continuous & (- f) | X is continuous )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g | X is continuous by A1, Th23;
then A2: ( ||.g.|| | X is continuous & (- g) | X is continuous ) by A1, NFCONT_3:22;
hence  |.f.| | X is continuous by Th9; ::_thesis: (- f) | X is continuous
 - g = - f by Th8;
hence  (- f) | X is continuous by A2, Th23; ::_thesis: verum
end;

theorem :: NFCONT_4:30
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) st f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 holds
f | REAL is continuous
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 holds
f | REAL is continuous
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 implies f | REAL is continuous )
assume A1: ( f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) ) ; ::_thesis: ( for x0 being real number holds not f is_continuous_in x0 or f | REAL is continuous )
given x0 being real number  such that A2: f is_continuous_in x0 ; ::_thesis: f | REAL is continuous
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A3: now__::_thesis:_for_x1,_x2_being_real_number_holds_g_/._(x1_+_x2)_=_(g_/._x1)_+_(g_/._x2)
let x1, x2 be real number ; ::_thesis: g /. (x1 + x2) = (g /. x1) + (g /. x2)
A4: ( g /. x1 = f /. x1 & g /. x2 = f /. x2 ) by REAL_NS1:def_4;
thus g /. (x1 + x2) = f /. (x1 + x2) by REAL_NS1:def_4
.= (f /. x1) + (f /. x2) by A1
.= (g /. x1) + (g /. x2) by A4, REAL_NS1:2 ; ::_thesis: verum
end;
 g is_continuous_in x0 by A2, Th1;
then  g | REAL is continuous by A1, A3, NFCONT_3:23;
hence  f | REAL is continuous by Th23; ::_thesis: verum
end;

theorem :: NFCONT_4:31
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for Y being Subset of (REAL-NS n) st dom f is compact & f | (dom f) is continuous & Y = rng f holds
Y is compact
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for Y being Subset of (REAL-NS n) st dom f is compact & f | (dom f) is continuous & Y = rng f holds
Y is compact
let f be PartFunc of REAL,(REAL n); ::_thesis: for Y being Subset of (REAL-NS n) st dom f is compact & f | (dom f) is continuous & Y = rng f holds
Y is compact
let Y be Subset of (REAL-NS n); ::_thesis: ( dom f is compact & f | (dom f) is continuous & Y = rng f implies Y is compact )
assume A1: ( dom f is compact & f | (dom f) is continuous & Y = rng f ) ; ::_thesis: Y is compact
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g | (dom g) is continuous by A1, Th23;
hence  Y is compact by A1, NFCONT_3:24; ::_thesis: verum
end;

theorem :: NFCONT_4:32
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for Y being Subset of REAL
for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds
Z is compact
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for Y being Subset of REAL
for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds
Z is compact
let f be PartFunc of REAL,(REAL n); ::_thesis: for Y being Subset of REAL
for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds
Z is compact
let Y be Subset of REAL; ::_thesis: for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds
Z is compact
let Z be Subset of (REAL-NS n); ::_thesis: ( Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous implies Z is compact )
assume A1: ( Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous ) ; ::_thesis: Z is compact
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g | Y is continuous by A1, Th23;
hence  Z is compact by A1, NFCONT_3:25; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attrf is Lipschitzian  means :Def6: :: NFCONT_4:def 6
 ex g being PartFunc of REAL,(REAL-NS n) st
( g = f & g is Lipschitzian );
end;

:: deftheorem Def6 defines Lipschitzian NFCONT_4:def_6_:_
 for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is Lipschitzian iff ex g being PartFunc of REAL,(REAL-NS n) st
( g = f & g is Lipschitzian ) );

theorem Th33: :: NFCONT_4:33
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds
( f is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )
hereby  ::_thesis: ( ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) implies f is Lipschitzian )
assume  f is Lipschitzian ; ::_thesis: ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( g = f & g is Lipschitzian ) by Def6;
consider r being real number  such that
A2: ( 0 < r & ( for x1, x2 being real number st x1 in dom g & x2 in dom g holds
||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) ) ) by A1, NFCONT_3:def_3;
take r = r; ::_thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) )
thus  0 < r by A2; ::_thesis: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
thus  for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ::_thesis: verum
proof
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) )
assume  ( x1 in dom f & x2 in dom f ) ; ::_thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
then A3: ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) by A1, A2;
 ( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by A1, REAL_NS1:def_4;
hence  |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A3, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
end;
given r being real number  such that A4: ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ; ::_thesis: f is Lipschitzian
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_g_&_x2_in_dom_g_holds_
||.((g_/._x1)_-_(g_/._x2)).||_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom g & x2 in dom g implies ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) )
assume  ( x1 in dom g & x2 in dom g ) ; ::_thesis: ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2))
then A5: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A4;
 ( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by REAL_NS1:def_4;
hence  ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) by A5, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
then  g is Lipschitzian by A4, NFCONT_3:def_3;
hence  f is Lipschitzian by Def6; ::_thesis: verum
end;

theorem Th34: :: NFCONT_4:34
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n) st f = h holds
( f is Lipschitzian iff h is Lipschitzian )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n) st f = h holds
( f is Lipschitzian iff h is Lipschitzian )
let f be PartFunc of REAL,(REAL n); ::_thesis: for h being PartFunc of REAL,(REAL-NS n) st f = h holds
( f is Lipschitzian iff h is Lipschitzian )
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = h implies ( f is Lipschitzian iff h is Lipschitzian ) )
assume A1: f = h ; ::_thesis: ( f is Lipschitzian iff h is Lipschitzian )
hereby  ::_thesis: ( h is Lipschitzian implies f is Lipschitzian )
assume  f is Lipschitzian ; ::_thesis: h is Lipschitzian
then consider r being real number  such that
A2: ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) by Th33;
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_h_&_x2_in_dom_h_holds_
||.((h_/._x1)_-_(h_/._x2)).||_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom h & x2 in dom h implies ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) )
assume  ( x1 in dom h & x2 in dom h ) ; ::_thesis: ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2))
then A3: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A2, A1;
 ( f /. x1 = h /. x1 & f /. x2 = h /. x2 ) by A1, REAL_NS1:def_4;
hence  ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) by A3, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
hence  h is Lipschitzian by A2, NFCONT_3:def_3; ::_thesis: verum
end;
assume  h is Lipschitzian ; ::_thesis: f is Lipschitzian
then consider r being real number  such that
A4: ( 0 < r & ( for x1, x2 being real number st x1 in dom h & x2 in dom h holds
||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) ) ) by NFCONT_3:def_3;
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_f_&_x2_in_dom_f_holds_
|.((f_/._x1)_-_(f_/._x2)).|_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) )
assume  ( x1 in dom f & x2 in dom f ) ; ::_thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
then A5: ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) by A4, A1;
 ( f /. x1 = h /. x1 & f /. x2 = h /. x2 ) by A1, REAL_NS1:def_4;
hence  |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A5, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum
end;
hence  f is Lipschitzian by A4, Th33; ::_thesis: verum
end;

theorem :: NFCONT_4:35
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n) holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )
proof
let n be Element of NAT ; ::_thesis: for X being set
for f being PartFunc of REAL,(REAL n) holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )
let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )
hereby  ::_thesis: ( ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) implies f | X is Lipschitzian )
assume  f | X is Lipschitzian ; ::_thesis: ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) )
then consider r being real number  such that
A1: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) ) ) by Th33;
take r = r; ::_thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) )
thus  0 < r by A1; ::_thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
thus  for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ::_thesis: verum
proof
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) )
assume A2: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
then  |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) by A1;
then  |.((f /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) by A2, PARTFUN2:15;
hence  |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A2, PARTFUN2:15; ::_thesis: verum
end;
end;
given r being real number  such that A3: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ; ::_thesis: f | X is Lipschitzian
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_(f_|_X)_&_x2_in_dom_(f_|_X)_holds_
|.(((f_|_X)_/._x1)_-_((f_|_X)_/._x2)).|_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) )
assume A4: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2))
then  |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A3;
then  |.(((f | X) /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A4, PARTFUN2:15;
hence  |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) by A4, PARTFUN2:15; ::_thesis: verum
end;
hence  f | X is Lipschitzian by A3, Th33; ::_thesis: verum
end;

registration
let n be Element of NAT ;
cluster empty Function-like  ->  Lipschitzian for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is empty holds
b1 is Lipschitzian
proof
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is empty implies f is Lipschitzian )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
assume  f is empty ; ::_thesis: f is Lipschitzian
then  g is empty ;
hence  f is Lipschitzian by Th34; ::_thesis: verum
end;
end;

registration
let n be Element of NAT ;
cluster empty Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() for Element of bool [:REAL,(REAL n):];
existence
 ex b1 being PartFunc of REAL,(REAL n) st b1 is empty
proof
take  the empty PartFunc of REAL,(REAL n) ; ::_thesis: the empty PartFunc of REAL,(REAL n) is empty
thus  the empty PartFunc of REAL,(REAL n) is empty ; ::_thesis: verum
end;
end;

registration
let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
let X be set ;
clusterf | X ->  Lipschitzian for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is Lipschitzian
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g is Lipschitzian by Th34;
then  g | X is Lipschitzian ;
hence  for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is Lipschitzian by Th34; ::_thesis: verum
end;
end;

theorem :: NFCONT_4:36
for n being Element of NAT
for X, X1 being set
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
proof
let n be Element of NAT ; ::_thesis: for X, X1 being set
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian & X1 c= X implies f | X1 is Lipschitzian )
assume that
A1: f | X is Lipschitzian and
A2: X1 c= X ; ::_thesis: f | X1 is Lipschitzian
 f | X1 = (f | X) | X1 by A2, RELAT_1:74;
hence  f | X1 is Lipschitzian by A1; ::_thesis: verum
end;

registration
let n be Element of NAT ;
let f1, f2 be Lipschitzian PartFunc of REAL,(REAL n);
clusterf1 + f2 ->  Lipschitzian for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is Lipschitzian
proof
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A1: ( g1 is Lipschitzian & g2 is Lipschitzian ) by Th34;
 g1 + g2 = f1 + f2 by Th5;
hence  for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is Lipschitzian by A1, Th34; ::_thesis: verum
end;
clusterf1 - f2 ->  Lipschitzian for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f1 - f2 holds
b1 is Lipschitzian
proof
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A2: ( g1 is Lipschitzian & g2 is Lipschitzian ) by Th34;
 g1 - g2 = f1 - f2 by Th10;
hence  for b1 being PartFunc of REAL,(REAL n) st b1 = f1 - f2 holds
b1 is Lipschitzian by A2, Th34; ::_thesis: verum
end;
end;

theorem :: NFCONT_4:37
for n being Element of NAT
for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
proof
let n be Element of NAT ; ::_thesis: for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 + f2) | (X /\ X1) is Lipschitzian )
assume A1: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 + f2) | (X /\ X1) is Lipschitzian
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 ( g1 | X is Lipschitzian & g2 | X1 is Lipschitzian ) by Th34, A1;
then A2: (g1 + g2) | (X /\ X1) is Lipschitzian by NFCONT_3:28;
 g1 + g2 = f1 + f2 by Th5;
hence  (f1 + f2) | (X /\ X1) is Lipschitzian by A2, Th34; ::_thesis: verum
end;

theorem :: NFCONT_4:38
for n being Element of NAT
for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian
proof
let n be Element of NAT ; ::_thesis: for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian
let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 - f2) | (X /\ X1) is Lipschitzian )
assume A1: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 - f2) | (X /\ X1) is Lipschitzian
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 ( g1 | X is Lipschitzian & g2 | X1 is Lipschitzian ) by Th34, A1;
then A2: (g1 - g2) | (X /\ X1) is Lipschitzian by NFCONT_3:29;
 g1 - g2 = f1 - f2 by Th10;
hence  (f1 - f2) | (X /\ X1) is Lipschitzian by A2, Th34; ::_thesis: verum
end;

registration
let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
let p be Real;
clusterp (#) f ->  Lipschitzian for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = p (#) f holds
b1 is Lipschitzian
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
A1: g is Lipschitzian by Th34;
 p (#) g = p (#) f by Th6;
hence  for b1 being PartFunc of REAL,(REAL n) st b1 = p (#) f holds
b1 is Lipschitzian by A1, Th34; ::_thesis: verum
end;
end;

theorem :: NFCONT_4:39
for n being Element of NAT
for X being set
for p being Real
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
proof
let n be Element of NAT ; ::_thesis: for X being set
for p being Real
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
let X be set ; ::_thesis: for p being Real
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
let p be Real; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian )
assume A1: ( f | X is Lipschitzian & X c= dom f ) ; ::_thesis: (p (#) f) | X is Lipschitzian
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g | X is Lipschitzian by Th34, A1;
then A2: (p (#) g) | X is Lipschitzian by A1, NFCONT_3:30;
 p (#) g = p (#) f by Th6;
hence  (p (#) f) | X is Lipschitzian by A2, Th34; ::_thesis: verum
end;

registration
let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
cluster|.f.| ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = |.f.| holds
b1 is Lipschitzian
proof
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g is Lipschitzian by Th34;
then  ||.g.|| is Lipschitzian ;
hence  for b1 being PartFunc of REAL,REAL st b1 = |.f.| holds
b1 is Lipschitzian by Th9; ::_thesis: verum
end;
end;

theorem :: NFCONT_4:40
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
proof
let n be Element of NAT ; ::_thesis: for X being set
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian implies ( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian ) )
assume A1: f | X is Lipschitzian ; ::_thesis: ( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g | X is Lipschitzian by A1, Th34;
then A2: ( - (g | X) is Lipschitzian & ||.g.|| | X is Lipschitzian & (- g) | X is Lipschitzian ) by NFCONT_3:31;
 - (g | X) = - (f | X) by Th8;
hence  - (f | X) is Lipschitzian by A2, Th34; ::_thesis: ( |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
thus  |.f.| | X is Lipschitzian by A2, Th9; ::_thesis: (- f) | X is Lipschitzian
 - g = - f by Th8;
hence  (- f) | X is Lipschitzian by A2, Th34; ::_thesis: verum
end;

registration
let n be Element of NAT ;
cluster Function-like constant  ->  Lipschitzian for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is constant holds
b1 is Lipschitzian
proof
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is constant implies f is Lipschitzian )
assume A1: f is constant ; ::_thesis: f is Lipschitzian
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
 g is constant by A1;
hence  f is Lipschitzian by Th34; ::_thesis: verum
end;
end;

registration
let n be Element of NAT ;
cluster Function-like Lipschitzian  ->  continuous for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is Lipschitzian holds
b1 is continuous
proof
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is Lipschitzian implies f is continuous )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
assume  f is Lipschitzian ; ::_thesis: f is continuous
then  g is Lipschitzian by Th34;
hence  f is continuous by Th23; ::_thesis: verum
end;
end;

theorem :: NFCONT_4:41
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
proof
let n be Element of NAT ; ::_thesis: for X being set
for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let f be PartFunc of REAL,(REAL n); ::_thesis: for r, p being Element of REAL n st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let r, p be Element of REAL n; ::_thesis: ( ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) implies f | X is continuous )
assume A1: for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ; ::_thesis: f | X is continuous
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4;
reconsider r0 = r, p0 = p as Point of (REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_x0_being_real_number_st_x0_in_X_holds_
g_/._x0_=_(x0_*_r0)_+_p0
let x0 be real number ; ::_thesis: ( x0 in X implies g /. x0 = (x0 * r0) + p0 )
assume A2: x0 in X ; ::_thesis: g /. x0 = (x0 * r0) + p0
A3: x0 * r = x0 * r0 by REAL_NS1:3;
thus g /. x0 = f /. x0 by REAL_NS1:def_4
.= (x0 * r) + p by A2, A1
.= (x0 * r0) + p0 by A3, REAL_NS1:2 ; ::_thesis: verum
end;
then  g | X is continuous by NFCONT_3:33;
hence  f | X is continuous by Th23; ::_thesis: verum
end;

theorem Th42: :: NFCONT_4:42
for n, i being Element of NAT
for x0 being Element of REAL n st 1 <= i & i <= n holds
proj (i,n) is_continuous_in x0
proof
let n, i be Element of NAT ; ::_thesis: for x0 being Element of REAL n st 1 <= i & i <= n holds
proj (i,n) is_continuous_in x0
let x0 be Element of REAL n; ::_thesis: ( 1 <= i & i <= n implies proj (i,n) is_continuous_in x0 )
assume A1: ( 1 <= i & i <= n ) ; ::_thesis: proj (i,n) is_continuous_in x0
A2: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
reconsider prg = proj (i,n) as PartFunc of (REAL-NS n),REAL by REAL_NS1:def_4;
reconsider px0 = x0 as Element of (REAL-NS n) by REAL_NS1:def_4;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_px1_being_Element_of_(REAL-NS_n)_st_px1_in_dom_prg_&_||.(px1_-_px0).||_<_s_holds_
|.(((proj_(i,n))_/._px1)_-_((proj_(i,n))_/._px0)).|_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) ) )
assume A3: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) )
take s = r; ::_thesis: ( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) )
thus  0 < s by A3; ::_thesis: for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r
now__::_thesis:_for_px1_being_Element_of_(REAL-NS_n)_st_px1_in_dom_prg_&_||.(px1_-_px0).||_<_r_holds_
|.(((proj_(i,n))_/._px1)_-_((proj_(i,n))_/._px0)).|_<_r
let px1 be Element of (REAL-NS n); ::_thesis: ( px1 in dom prg & ||.(px1 - px0).|| < r implies |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r )
assume A4: ( px1 in dom prg & ||.(px1 - px0).|| < r ) ; ::_thesis: |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r
reconsider x1 = px1 as Element of REAL n by REAL_NS1:def_4;
A5: ||.(px1 - px0).|| = |.(x1 - x0).| by REAL_NS1:1, REAL_NS1:5;
 (proj (i,n)) /. (x1 - x0) = ((proj (i,n)) /. x1) - ((proj (i,n)) /. x0) by A1, PDIFF_8:12;
then  |.(((proj (i,n)) /. x1) - ((proj (i,n)) /. x0)).| <= |.(x1 - x0).| by A1, PDIFF_8:5;
hence  |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r by A4, A5, XXREAL_0:2; ::_thesis: verum
end;
hence  for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ; ::_thesis: verum
end;
then  prg is_continuous_in px0 by A2, NFCONT_1:8;
hence  proj (i,n) is_continuous_in x0 by Def4; ::_thesis: verum
end;

theorem Th43: :: NFCONT_4:43
for x0 being real number
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) holds
( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )
proof
let x0 be real number ; ::_thesis: for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) holds
( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )
let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) holds
( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )
let h be PartFunc of REAL,(REAL n); ::_thesis: ( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )
hereby  ::_thesis: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) implies h is_continuous_in x0 )
assume A1: h is_continuous_in x0 ; ::_thesis: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) )
hence A2: x0 in dom h by Th3; ::_thesis: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0
thus  for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 )
assume  i in Seg n ; ::_thesis: (proj (i,n)) * h is_continuous_in x0
then A3: ( 1 <= i & i <= n ) by FINSEQ_1:1;
A4: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
 rng h c= REAL n ;
then A5: dom ((proj (i,n)) * h) = dom h by A4, RELAT_1:27;
 proj (i,n) is_continuous_in h /. x0 by A3, Th42;
hence  (proj (i,n)) * h is_continuous_in x0 by A5, A1, A2, Th22; ::_thesis: verum
end;
end;
assume A6: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) ; ::_thesis: h is_continuous_in x0
 for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r ) )
proof
let r0 be Real; ::_thesis: ( 0 < r0 implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) ) )
assume A7: 0 < r0 ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) )
set r = r0 / 2;
A8: 0 < r0 / 2 by A7, XREAL_1:215;
defpred S1[ Nat, real number ] means ( 0 < $2 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < $2 holds
|.((((proj ($1,n)) * h) . x1) - (((proj ($1,n)) * h) . x0)).| < (r0 / 2) / n ) );
A9: 0 < (r0 / 2) / n by A8, XREAL_1:139;
A10: for j being Nat st j in Seg n holds
ex x being Element of REAL st S1[j,x]
proof
let j be Nat; ::_thesis: ( j in Seg n implies ex x being Element of REAL st S1[j,x] )
assume A11: j in Seg n ; ::_thesis: ex x being Element of REAL st S1[j,x]
A12: (proj (j,n)) * h is_continuous_in x0 by A6, A11;
A13: dom (proj (j,n)) = REAL n by FUNCT_2:def_1;
 rng h c= REAL n ;
then A14: dom ((proj (j,n)) * h) = dom h by A13, RELAT_1:27;
consider sj being real number  such that
A15: ( 0 < sj & ( for x1 being real number st x1 in dom ((proj (j,n)) * h) & abs (x1 - x0) < sj holds
|.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n ) ) by A12, A9, FCONT_1:3;
 sj is Real by XREAL_0:def_1;
hence  ex x being Element of REAL st S1[j,x] by A15, A14; ::_thesis: verum
end;
consider s0 being FinSequence of REAL  such that
A16: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S1[k,s0 . k] ) ) from FINSEQ_1:sch_5(A10);
 n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by A16, FUNCT_1:3;
 rng s0 is finite by A16, FINSET_1:8;
then reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set ;
A17: min rs0 in rng s0 by XXREAL_2:def_7;
then reconsider s = min rs0 as Real ;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) )
 ex i1 being set st
( i1 in dom s0 & s = s0 . i1 ) by A17, FUNCT_1:def_3;
hence  0 < s by A16; ::_thesis: for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0
now__::_thesis:_for_x1_being_real_number_st_x1_in_dom_h_&_abs_(x1_-_x0)_<_s_holds_
|.((h_/._x1)_-_(h_/._x0)).|_<_r0
let x1 be real number ; ::_thesis: ( x1 in dom h & abs (x1 - x0) < s implies |.((h /. x1) - (h /. x0)).| < r0 )
assume A18: ( x1 in dom h & abs (x1 - x0) < s ) ; ::_thesis: |.((h /. x1) - (h /. x0)).| < r0
now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_
|.((proj_(j,n))_._((h_/._x1)_-_(h_/._x0))).|_<=_(r0_/_2)_/_n
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n )
assume  ( 1 <= j & j <= n ) ; ::_thesis: |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n
then A19: j in Seg n by FINSEQ_1:1;
then  s0 . j in rng s0 by A16, FUNCT_1:3;
then  s <= s0 . j by XXREAL_2:def_7;
then  abs (x1 - x0) < s0 . j by A18, XXREAL_0:2;
then A20: |.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n by A19, A18, A16;
A21: ((proj (j,n)) * h) . x1 = (proj (j,n)) . (h . x1) by A18, FUNCT_1:13
.= (proj (j,n)) . (h /. x1) by A18, PARTFUN1:def_6 ;
((proj (j,n)) * h) . x0 = (proj (j,n)) . (h . x0) by A6, FUNCT_1:13
.= (proj (j,n)) . (h /. x0) by A6, PARTFUN1:def_6 ;
hence  |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n by A20, A21, PDIFF_8:12; ::_thesis: verum
end;
then  |.((h /. x1) - (h /. x0)).| <= n * ((r0 / 2) / n) by PDIFF_8:17;
then A22: |.((h /. x1) - (h /. x0)).| <= r0 / 2 by XCMPLX_1:87;
 r0 / 2 < r0 by A7, XREAL_1:216;
hence  |.((h /. x1) - (h /. x0)).| < r0 by A22, XXREAL_0:2; ::_thesis: verum
end;
hence  for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ; ::_thesis: verum
end;
hence  h is_continuous_in x0 by A6, Th3; ::_thesis: verum
end;

theorem :: NFCONT_4:44
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) holds
( h is continuous iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous )
proof
let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) holds
( h is continuous iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous )
let h be PartFunc of REAL,(REAL n); ::_thesis: ( h is continuous iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous )
hereby  ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous ) implies h is continuous )
assume A1: h is continuous ; ::_thesis: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous
thus  for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * h is continuous )
assume A2: i in Seg n ; ::_thesis: (proj (i,n)) * h is continuous
A3: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
 rng h c= REAL n ;
then A4: dom ((proj (i,n)) * h) = dom h by A3, RELAT_1:27;
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_((proj_(i,n))_*_h)_holds_
(proj_(i,n))_*_h_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom ((proj (i,n)) * h) implies (proj (i,n)) * h is_continuous_in x0 )
assume  x0 in dom ((proj (i,n)) * h) ; ::_thesis: (proj (i,n)) * h is_continuous_in x0
then  h is_continuous_in x0 by A1, A4, Def5;
hence  (proj (i,n)) * h is_continuous_in x0 by A2, Th43; ::_thesis: verum
end;
hence  (proj (i,n)) * h is continuous by FCONT_1:def_2; ::_thesis: verum
end;
end;
assume A5: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous ; ::_thesis: h is continuous
let x0 be real number ; :: according to NFCONT_4:def_5 ::_thesis: ( x0 in dom h implies h is_continuous_in x0 )
assume A6: x0 in dom h ; ::_thesis: h is_continuous_in x0
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(proj_(i,n))_*_h_is_continuous_in_x0
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 )
assume A7: i in Seg n ; ::_thesis: (proj (i,n)) * h is_continuous_in x0
A8: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
 rng h c= REAL n ;
then A9: dom ((proj (i,n)) * h) = dom h by A8, RELAT_1:27;
 (proj (i,n)) * h is continuous by A5, A7;
hence  (proj (i,n)) * h is_continuous_in x0 by A6, A9, FCONT_1:def_2; ::_thesis: verum
end;
hence  h is_continuous_in x0 by A6, Th43; ::_thesis: verum
end;

theorem Th45: :: NFCONT_4:45
for n, i being Element of NAT
for x0 being Point of (REAL-NS n) st 1 <= i & i <= n holds
Proj (i,n) is_continuous_in x0
proof
let n, i be Element of NAT ; ::_thesis: for x0 being Point of (REAL-NS n) st 1 <= i & i <= n holds
Proj (i,n) is_continuous_in x0
let x0 be Point of (REAL-NS n); ::_thesis: ( 1 <= i & i <= n implies Proj (i,n) is_continuous_in x0 )
assume A1: ( 1 <= i & i <= n ) ; ::_thesis: Proj (i,n) is_continuous_in x0
A2: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x1_being_Point_of_(REAL-NS_n)_st_x1_in_dom_(Proj_(i,n))_&_||.(x1_-_x0).||_<_s_holds_
||.(((Proj_(i,n))_/._x1)_-_((Proj_(i,n))_/._x0)).||_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) ) )
assume A3: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) )
take s = r; ::_thesis: ( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) )
thus  0 < s by A3; ::_thesis: for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r
now__::_thesis:_for_x1_being_Point_of_(REAL-NS_n)_st_x1_in_dom_(Proj_(i,n))_&_||.(x1_-_x0).||_<_s_holds_
||.(((Proj_(i,n))_/._x1)_-_((Proj_(i,n))_/._x0)).||_<_r
let x1 be Point of (REAL-NS n); ::_thesis: ( x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s implies ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r )
assume A4: ( x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r
 (Proj (i,n)) /. (x1 - x0) = ((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0) by A1, PDIFF_8:11;
then  ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| <= ||.(x1 - x0).|| by A1, PDIFF_8:3;
hence  ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r by A4, XXREAL_0:2; ::_thesis: verum
end;
hence  for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ; ::_thesis: verum
end;
hence  Proj (i,n) is_continuous_in x0 by A2, NFCONT_1:7; ::_thesis: verum
end;

theorem Th46: :: NFCONT_4:46
for x0 being real number
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL-NS n) holds
( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 )
proof
let x0 be real number ; ::_thesis: for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL-NS n) holds
( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 )
let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL-NS n) holds
( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 )
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 )
hereby  ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 ) implies h is_continuous_in x0 )
assume A1: h is_continuous_in x0 ; ::_thesis: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0
then A2: x0 in dom h by NFCONT_3:7;
thus  for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (Proj (i,n)) * h is_continuous_in x0 )
assume  i in Seg n ; ::_thesis: (Proj (i,n)) * h is_continuous_in x0
then A3: ( 1 <= i & i <= n ) by FINSEQ_1:1;
A4: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
 rng h c= the carrier of (REAL-NS n) ;
then A5: dom ((Proj (i,n)) * h) = dom h by A4, RELAT_1:27;
 Proj (i,n) is_continuous_in h /. x0 by A3, Th45;
hence  (Proj (i,n)) * h is_continuous_in x0 by A2, A5, A1, NFCONT_3:15; ::_thesis: verum
end;
end;
assume A6: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 ; ::_thesis: h is_continuous_in x0
 1 <= n by NAT_1:14;
then  1 in Seg n by FINSEQ_1:1;
then  (Proj (1,n)) * h is_continuous_in x0 by A6;
then A7: x0 in dom ((Proj (1,n)) * h) by NFCONT_3:8;
A8: dom ((Proj (1,n)) * h) c= dom h by RELAT_1:25;
 for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r ) )
proof
let r0 be Real; ::_thesis: ( 0 < r0 implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r0 ) ) )
set r = r0 / 2;
assume A9: 0 < r0 ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r0 ) )
then A10: 0 < r0 / 2 by XREAL_1:215;
defpred S1[ set , real number ] means  ex j being Element of NAT st
( $1 = j & 0 < $2 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < $2 holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) );
A11: 0 < (r0 / 2) / n by A10, XREAL_1:139;
A12: for j0 being Nat st j0 in Seg n holds
ex x being Element of REAL st S1[j0,x]
proof
let j0 be Nat; ::_thesis: ( j0 in Seg n implies ex x being Element of REAL st S1[j0,x] )
assume A13: j0 in Seg n ; ::_thesis: ex x being Element of REAL st S1[j0,x]
reconsider j = j0 as Element of NAT by ORDINAL1:def_12;
A14: (Proj (j,n)) * h is_continuous_in x0 by A6, A13;
A15: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
 rng h c= the carrier of (REAL-NS n) ;
then A16: dom ((Proj (j,n)) * h) = dom h by A15, RELAT_1:27;
consider sj being real number  such that
A17: ( 0 < sj & ( for x1 being real number st x1 in dom ((Proj (j,n)) * h) & abs (x1 - x0) < sj holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A14, A11, NFCONT_3:8;
 sj is Real by XREAL_0:def_1;
hence  ex x being Element of REAL st S1[j0,x] by A17, A16; ::_thesis: verum
end;
consider s0 being FinSequence of REAL  such that
A18: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S1[k,s0 . k] ) ) from FINSEQ_1:sch_5(A12);
 n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by A18, FUNCT_1:3;
 rng s0 is finite by A18, FINSET_1:8;
then reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set ;
A19: min rs0 in rng s0 by XXREAL_2:def_7;
then reconsider s = min rs0 as Real ;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r0 ) )
consider i1 being set  such that
A20: ( i1 in dom s0 & s = s0 . i1 ) by A19, FUNCT_1:def_3;
 ex j being Element of NAT st
( i1 = j & 0 < s0 . i1 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . i1 holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A18, A20;
hence  0 < s by A20; ::_thesis: for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r0
let x1 be real number ; ::_thesis: ( x1 in dom h & abs (x1 - x0) < s implies ||.((h /. x1) - (h /. x0)).|| < r0 )
assume A21: ( x1 in dom h & abs (x1 - x0) < s ) ; ::_thesis: ||.((h /. x1) - (h /. x0)).|| < r0
now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_
||.((Proj_(j,n))_._((h_/._x1)_-_(h_/._x0))).||_<=_(r0_/_2)_/_n
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n )
assume  ( 1 <= j & j <= n ) ; ::_thesis: ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n
then A22: j in Seg n by FINSEQ_1:1;
then consider jj being Element of NAT  such that
A23: ( jj = j & 0 < s0 . j & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . j holds
||.((((Proj (jj,n)) * h) /. x1) - (((Proj (jj,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A18;
 s0 . j in rng s0 by A22, A18, FUNCT_1:3;
then  s <= s0 . j by XXREAL_2:def_7;
then  abs (x1 - x0) < s0 . j by A21, XXREAL_0:2;
then A24: ||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n by A23, A21;
A25: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
then A26: ((Proj (j,n)) * h) /. x1 = (Proj (j,n)) /. (h /. x1) by A21, PARTFUN2:4;
 ((Proj (j,n)) * h) /. x0 = (Proj (j,n)) /. (h /. x0) by A25, A8, A7, PARTFUN2:4;
hence  ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n by A24, A26, PDIFF_8:11; ::_thesis: verum
end;
then  ||.((h /. x1) - (h /. x0)).|| <= n * ((r0 / 2) / n) by PDIFF_8:16;
then A27: ||.((h /. x1) - (h /. x0)).|| <= r0 / 2 by XCMPLX_1:87;
 r0 / 2 < r0 by A9, XREAL_1:216;
hence  ||.((h /. x1) - (h /. x0)).|| < r0 by A27, XXREAL_0:2; ::_thesis: verum
end;
hence  h is_continuous_in x0 by A8, A7, NFCONT_3:8; ::_thesis: verum
end;

theorem :: NFCONT_4:47
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL-NS n) holds
( h is continuous iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous )
proof
let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL-NS n) holds
( h is continuous iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous )
let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( h is continuous iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous )
hereby  ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous ) implies h is continuous )
assume A1: h is continuous ; ::_thesis: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous
thus  for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (Proj (i,n)) * h is continuous )
assume A2: i in Seg n ; ::_thesis: (Proj (i,n)) * h is continuous
A3: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
 rng h c= the carrier of (REAL-NS n) ;
then A4: dom ((Proj (i,n)) * h) = dom h by A3, RELAT_1:27;
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_((Proj_(i,n))_*_h)_holds_
(Proj_(i,n))_*_h_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom ((Proj (i,n)) * h) implies (Proj (i,n)) * h is_continuous_in x0 )
assume  x0 in dom ((Proj (i,n)) * h) ; ::_thesis: (Proj (i,n)) * h is_continuous_in x0
then  h is_continuous_in x0 by A1, A4, NFCONT_3:def_2;
hence  (Proj (i,n)) * h is_continuous_in x0 by A2, Th46; ::_thesis: verum
end;
hence  (Proj (i,n)) * h is continuous by NFCONT_3:def_2; ::_thesis: verum
end;
end;
assume A5: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous ; ::_thesis: h is continuous
let x0 be real number ; :: according to NFCONT_3:def_2 ::_thesis: ( not x0 in dom h or h is_continuous_in x0 )
assume A6: x0 in dom h ; ::_thesis: h is_continuous_in x0
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(Proj_(i,n))_*_h_is_continuous_in_x0
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (Proj (i,n)) * h is_continuous_in x0 )
assume A7: i in Seg n ; ::_thesis: (Proj (i,n)) * h is_continuous_in x0
A8: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
 rng h c= the carrier of (REAL-NS n) ;
then A9: dom ((Proj (i,n)) * h) = dom h by A8, RELAT_1:27;
 (Proj (i,n)) * h is continuous by A5, A7;
hence  (Proj (i,n)) * h is_continuous_in x0 by A6, A9, NFCONT_3:def_2; ::_thesis: verum
end;
hence  h is_continuous_in x0 by Th46; ::_thesis: verum
end;