environ
vocabularies HIDDEN, PRE_TOPC, NORMSP_1, FUNCT_1, ARYTM_1, NAT_1, SUBSET_1, NUMBERS, CARD_1, XXREAL_0, FUNCT_7, REAL_1, ARYTM_3, RELAT_1, ORDINAL2, SEQ_1, SEQ_2, POWER, RSSPACE3, LOPBAN_1, ORDEQ_01, STRUCT_0, COMPLEX1, VALUED_1, ALI2, SUPINF_2, XBOOLE_0, ABIAN, INTEGRA1, FINSEQ_1, TARSKI, INTEGRA5, CARD_3, XXREAL_1, PARTFUN1, RLVECT_1, SEQ_4, FUNCT_2, RCOMP_1, VALUED_0, XXREAL_2, FCONT_1, ALGSTR_0, CFCONT_1, MEASURE5, RLSUB_1, RELAT_2, REWRITE1, NFCONT_1, C0SP2, RSSPACE, RSSPACE4, FUNCOP_1, REALSET1, FDIFF_1, PREPOWER, INTEGRA7, METRIC_1, SERIES_1, SIN_COS, SEQFUNC, REAL_NS1, FINSEQ_2, EUCLID, NEWTON, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, PARTFUN2, NUMBERS, XXREAL_0, XREAL_0, REAL_1, NAT_1, VALUED_0, COMPLEX1, XCMPLX_0, XXREAL_2, FUNCOP_1, FINSEQ_1, VALUED_1, FINSEQ_2, SEQ_1, SEQ_2, NEWTON, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1, FUNCT_7, ABIAN, PREPOWER, POWER, SERIES_1, SEQFUNC, MEASURE5, SIN_COS, TAYLOR_1, INTEGRA1, INTEGRA5, INTEGRA7, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, VFUNCT_1, RSSPACE, EUCLID, RSSPACE3, LOPBAN_1, NFCONT_1, INTEGR19, RSSPACE4, REAL_NS1, PDIFF_1, INTEGR15, INTEGR18, NFCONT_3, NDIFF_3, NFCONT_2, NFCONT_4;
definitions ABIAN, NORMSP_0, FDIFF_1, RLSUB_1, INTEGR15, NFCONT_2;
theorems ABSVALUE, RLVECT_1, NORMSP_0, XCMPLX_1, SEQ_1, SEQ_2, SERIES_1, TAYLOR_1, PARTFUN1, PARTFUN2, FDIFF_2, INTEGRA7, FUNCT_1, NAT_1, POWER, FUNCT_2, NORMSP_1, XREAL_1, RSSPACE3, LOPBAN_1, FUNCT_7, XXREAL_0, XREAL_0, ORDINAL1, RELAT_1, TARSKI, RSSPACE4, RSSPACE, NFCONT_1, NFCONT_3, RLSUB_1, FCONT_1, SEQ_4, VFUNCT_1, NEWTON, XBOOLE_0, RCOMP_1, FUNCOP_1, CARD_1, NDIFF_3, SIN_COS, COMSEQ_2, INTEGRA2, XXREAL_1, RVSUM_1, COMPLEX1, NDIFF_4, PDIFF_1, FDIFF_1, ROLLE, VALUED_1, XBOOLE_1, INTEGR19, REAL_NS1, INTEGRA5, PREPOWER, NFCONT_4, HOLDER_1, INT_1, RELSET_1, NFCONT_2;
schemes SEQ_1, NAT_1, XBOOLE_0, FUNCT_2, PARTFUN2;
registrations STRUCT_0, NAT_1, VALUED_1, NORMSP_0, XXREAL_0, NUMBERS, XBOOLE_0, FUNCT_1, FUNCT_2, XREAL_0, MEMBERED, NORMSP_1, RELAT_1, FINSEQ_2, RELSET_1, INTEGRA1, ORDINAL1, FUNCOP_1, NEWTON, NFCONT_3, XXREAL_2, RSSPACE4, RCOMP_1, RLVECT_1, REAL_NS1, VALUED_0, FINSEQ_1, FDIFF_1, FCONT_1, EUCLID, MEASURE5, VALUED_2, FCONT_3, POWER, NFCONT_4, PREPOWER;
constructors HIDDEN, REAL_1, ABIAN, SEQ_1, SEQ_2, RSSPACE3, RELSET_1, SEQ_4, VFUNCT_1, PDIFF_1, INTEGRA5, NFCONT_3, RLSUB_1, PARTFUN2, FCONT_1, NFCONT_1, NDIFF_1, NDIFF_3, RSSPACE4, SEQFUNC, INTEGR18, RVSUM_1, BINOP_2, INTEGR19, INTEGR15, NFCONT_4, FDIFF_1, VALUED_2, PREPOWER, INTEGRA7, COMSEQ_2, COMSEQ_3, SIN_COS, TAYLOR_1, NFCONT_2, C0SP2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SUBSET_1, STRUCT_0, ALGSTR_0, NORMSP_0, RSSPACE4, RLVECT_1, FINSEQ_1, RCOMP_1, EUCLID, INTEGRA5;
expansions ABIAN, NORMSP_0, FDIFF_1, FINSEQ_1, INTEGRA5, NFCONT_2;
definition
let X be non
empty closed_interval Subset of
REAL;
let Y be
RealNormSpace;
func R_VectorSpace_of_ContinuousFunctions (
X,
Y)
-> strict RealLinearSpace equals
RLSStruct(#
(ContinuousFunctions (X,Y)),
(Zero_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),
(Add_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),
(Mult_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))) #);
coherence
RLSStruct(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Add_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Mult_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))) #) is strict RealLinearSpace
by RSSPACE:11;
end;
::
deftheorem defines
R_VectorSpace_of_ContinuousFunctions ORDEQ_01:def 3 :
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds R_VectorSpace_of_ContinuousFunctions (X,Y) = RLSStruct(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Add_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Mult_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))) #);
definition
let X be non
empty closed_interval Subset of
REAL;
let Y be
RealNormSpace;
func R_NormSpace_of_ContinuousFunctions (
X,
Y)
-> non
empty strict NORMSTR equals
NORMSTR(#
(ContinuousFunctions (X,Y)),
(Zero_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),
(Add_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),
(Mult_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),
(ContinuousFunctionsNorm (X,Y)) #);
coherence
NORMSTR(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Add_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Mult_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(ContinuousFunctionsNorm (X,Y)) #) is non empty strict NORMSTR
;
end;
::
deftheorem defines
R_NormSpace_of_ContinuousFunctions ORDEQ_01:def 6 :
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) = NORMSTR(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Add_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Mult_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(ContinuousFunctionsNorm (X,Y)) #);
Lm2:
for a being Real
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y)) holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
Lm3:
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds
( R_NormSpace_of_ContinuousFunctions (X,Y) is reflexive & R_NormSpace_of_ContinuousFunctions (X,Y) is discerning & R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace-like )
Lm4:
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace
registration
let X be non
empty closed_interval Subset of
REAL;
let Y be
RealNormSpace;
coherence
( R_NormSpace_of_ContinuousFunctions (X,Y) is reflexive & R_NormSpace_of_ContinuousFunctions (X,Y) is discerning & R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace-like & R_NormSpace_of_ContinuousFunctions (X,Y) is vector-distributive & R_NormSpace_of_ContinuousFunctions (X,Y) is scalar-distributive & R_NormSpace_of_ContinuousFunctions (X,Y) is scalar-associative & R_NormSpace_of_ContinuousFunctions (X,Y) is scalar-unital & R_NormSpace_of_ContinuousFunctions (X,Y) is Abelian & R_NormSpace_of_ContinuousFunctions (X,Y) is add-associative & R_NormSpace_of_ContinuousFunctions (X,Y) is right_zeroed & R_NormSpace_of_ContinuousFunctions (X,Y) is right_complementable )
by Lm4;
end;
Lm5:
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for C being Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) st C = ContinuousFunctions (X,Y) holds
C is closed
Lm6:
for X being non empty closed_interval Subset of REAL
for Y being RealBanachSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) is RealBanachSpace
theorem Th36:
for
n being non
zero Element of
NAT for
a,
b being
Real for
Z being
open Subset of
REAL for
y0 being
VECTOR of
(REAL-NS n) for
f being
continuous PartFunc of
REAL,
(REAL-NS n) for
g being
PartFunc of
REAL,
(REAL-NS n) st
a <= b &
dom f = ['a,b'] &
dom g = ['a,b'] &
Z = ].a,b.[ & ( for
t being
Real st
t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
(
g is
continuous &
g /. a = y0 &
g is_differentiable_on Z & ( for
t being
Real st
t in Z holds
diff (
g,
t)
= f /. t ) )
Lm7:
for n being non zero Element of NAT
for i being Nat holds (proj (i,n)) . (0. (REAL-NS n)) = 0
theorem Th43:
for
n being non
zero Element of
NAT for
a,
b being
Real for
Z being
open Subset of
REAL for
y0 being
VECTOR of
(REAL-NS n) for
y,
Gf being
continuous PartFunc of
REAL,
(REAL-NS n) for
g being
PartFunc of
REAL,
(REAL-NS n) st
a < b &
Z = ].a,b.[ &
dom y = ['a,b'] &
dom g = ['a,b'] &
dom Gf = ['a,b'] &
y is_differentiable_on Z &
y /. a = y0 & ( for
t being
Real st
t in Z holds
diff (
y,
t)
= Gf /. t ) & ( for
t being
Real st
t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) holds
y = g
theorem Th44:
for
n being non
zero Element of
NAT for
a,
b,
c,
d being
Real for
f being
PartFunc of
REAL,
(REAL-NS n) st
a <= b &
f is_integrable_on ['a,b'] &
||.f.|| is_integrable_on ['a,b'] &
f | ['a,b'] is
bounded &
['a,b'] c= dom f &
c in ['a,b'] &
d in ['a,b'] holds
(
||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] &
||.f.|| | ['(min (c,d)),(max (c,d))'] is
bounded &
||.(integral (f,c,d)).|| <= integral (
||.f.||,
(min (c,d)),
(max (c,d))) )
theorem Th45:
for
n being non
zero Element of
NAT for
a,
b,
c,
d,
e being
Real for
f being
PartFunc of
REAL,
(REAL-NS n) st
a <= b &
c <= d &
f is_integrable_on ['a,b'] &
||.f.|| is_integrable_on ['a,b'] &
f | ['a,b'] is
bounded &
['a,b'] c= dom f &
c in ['a,b'] &
d in ['a,b'] & ( for
x being
Real st
x in ['c,d'] holds
||.(f /. x).|| <= e ) holds
(
||.(integral (f,c,d)).|| <= e * (d - c) &
||.(integral (f,d,c)).|| <= e * (d - c) )
Lm8:
for a being Real
for g being Function of REAL,REAL st ( for x being Real holds g . x = x - a ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = 1 )
Lm9:
for n being Nat
for a, r, L being Real
for g being Function of REAL,REAL st ( for x being Real holds g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) )
Lm10:
for m being non zero Element of NAT
for a, r, L being Real
for g being Function of REAL,REAL st ( for x being Real holds g . x = r * ((((r * (x - a)) |^ m) / (m !)) * L) ) holds
for x being Real holds g is_differentiable_in x
Lm11:
for n being non zero Element of NAT
for a, r, t, L being Real
for f0 being Function of REAL,REAL st a <= t & ( for x being Real holds f0 . x = r * ((((r * (x - a)) |^ n) / (n !)) * L) ) holds
( f0 | ['a,t'] is continuous & f0 | ['a,t'] is bounded & f0 is_integrable_on ['a,t'] & integral (f0,a,t) = (((r * (t - a)) |^ (n + 1)) / ((n + 1) !)) * L )
Lm12:
for a, t, L, r being Real
for k being non zero Element of NAT st a <= t holds
ex rg being PartFunc of REAL,REAL st
( dom rg = ['a,t'] & ( for x being Real st x in ['a,t'] holds
rg . x = r * ((((r * (x - a)) |^ k) / (k !)) * L) ) & rg is continuous & rg is_integrable_on ['a,t'] & rg | ['a,t'] is bounded & integral (rg,a,t) = (((r * (t - a)) |^ (k + 1)) / ((k + 1) !)) * L )
theorem Th48:
for
a,
t being
Real for
f,
g being
PartFunc of
REAL,
REAL st
a <= t &
['a,t'] c= dom f &
f is_integrable_on ['a,t'] &
f | ['a,t'] is
bounded &
['a,t'] c= dom g &
g is_integrable_on ['a,t'] &
g | ['a,t'] is
bounded & ( for
x being
Real st
x in ['a,t'] holds
f . x <= g . x ) holds
integral (
f,
a,
t)
<= integral (
g,
a,
t)
definition
let n be non
zero Element of
NAT ;
let y0 be
VECTOR of
(REAL-NS n);
let G be
Function of
(REAL-NS n),
(REAL-NS n);
let a,
b be
Real;
assume A1:
(
a <= b &
G is_continuous_on dom G )
;
func Fredholm (
G,
a,
b,
y0)
-> Function of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))),
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) means :
Def7:
for
x being
VECTOR of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ex
f,
g,
Gf being
continuous PartFunc of
REAL,
(REAL-NS n) st
(
x = f &
it . x = g &
dom f = ['a,b'] &
dom g = ['a,b'] &
Gf = G * f & ( for
t being
Real st
t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) );
existence
ex b1 being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))),(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) st
for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ex f, g, Gf being continuous PartFunc of REAL,(REAL-NS n) st
( x = f & b1 . x = g & dom f = ['a,b'] & dom g = ['a,b'] & Gf = G * f & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) )
uniqueness
for b1, b2 being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))),(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) st ( for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ex f, g, Gf being continuous PartFunc of REAL,(REAL-NS n) st
( x = f & b1 . x = g & dom f = ['a,b'] & dom g = ['a,b'] & Gf = G * f & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) ) ) & ( for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ex f, g, Gf being continuous PartFunc of REAL,(REAL-NS n) st
( x = f & b2 . x = g & dom f = ['a,b'] & dom g = ['a,b'] & Gf = G * f & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) ) ) holds
b1 = b2
end;
::
deftheorem Def7 defines
Fredholm ORDEQ_01:def 7 :
for n being non zero Element of NAT
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for a, b being Real st a <= b & G is_continuous_on dom G holds
for b6 being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))),(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) holds
( b6 = Fredholm (G,a,b,y0) iff for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ex f, g, Gf being continuous PartFunc of REAL,(REAL-NS n) st
( x = f & b6 . x = g & dom f = ['a,b'] & dom g = ['a,b'] & Gf = G * f & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) ) );
theorem Th49:
for
n being non
zero Element of
NAT for
a,
b,
r being
Real for
y0 being
VECTOR of
(REAL-NS n) for
G being
Function of
(REAL-NS n),
(REAL-NS n) st
a <= b &
0 < r & ( for
y1,
y2 being
VECTOR of
(REAL-NS n) holds
||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for
u,
v being
VECTOR of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) for
g,
h being
continuous PartFunc of
REAL,
(REAL-NS n) st
g = (Fredholm (G,a,b,y0)) . u &
h = (Fredholm (G,a,b,y0)) . v holds
for
t being
Real st
t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||
theorem Th50:
for
n being non
zero Element of
NAT for
a,
b,
r being
Real for
y0 being
VECTOR of
(REAL-NS n) for
G being
Function of
(REAL-NS n),
(REAL-NS n) st
a <= b &
0 < r & ( for
y1,
y2 being
VECTOR of
(REAL-NS n) holds
||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for
u,
v being
VECTOR of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) for
m being
Element of
NAT for
g,
h being
continuous PartFunc of
REAL,
(REAL-NS n) st
g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u &
h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds
for
t being
Real st
t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
Lm13:
for r, L, a, b, t being Real
for m being Nat st a <= t & t <= b & 0 <= L & 0 <= r holds
(((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * L <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * L
Lm14:
for a, b, r being Real st a < b & 0 < r holds
ex m being Element of NAT st
( ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) < 1 & 0 < ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) )
theorem Th51:
for
n being non
zero Element of
NAT for
a,
b,
r being
Real for
y0 being
VECTOR of
(REAL-NS n) for
G being
Function of
(REAL-NS n),
(REAL-NS n) for
m being
Nat st
a <= b &
0 < r & ( for
y1,
y2 being
VECTOR of
(REAL-NS n) holds
||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for
u,
v being
VECTOR of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) holds
||.(((iter ((Fredholm (G,a,b,y0)),(m + 1))) . u) - ((iter ((Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
theorem Th54:
for
n being non
zero Element of
NAT for
a,
b being
Real for
Z being
open Subset of
REAL for
y0 being
VECTOR of
(REAL-NS n) for
G being
Function of
(REAL-NS n),
(REAL-NS n) for
f,
g being
continuous PartFunc of
REAL,
(REAL-NS n) st
dom f = ['a,b'] &
dom g = ['a,b'] &
Z = ].a,b.[ &
a < b &
G is_Lipschitzian_on the
carrier of
(REAL-NS n) &
g = (Fredholm (G,a,b,y0)) . f holds
(
g /. a = y0 &
g is_differentiable_on Z & ( for
t being
Real st
t in Z holds
diff (
g,
t)
= (G * f) /. t ) )