:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received December 31, 2013

:: Copyright (c) 2013-2018 Association of Mizar Users

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

Lm1: the carrier of (REAL-NS 1) = REAL 1

by REAL_NS1:def 4;

Lm2: ( dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds

( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )

proof end;

theorem NDIFF435: :: ORDEQ_02:1

for Y being RealNormSpace

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

proof end;

theorem :: ORDEQ_02:2

for Y being RealNormSpace

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

proof end;

theorem FTh40: :: ORDEQ_02:3

for Y being RealNormSpace

for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds

( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) )

for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds

( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) )

proof end;

theorem FTh41: :: ORDEQ_02:4

for Y being RealNormSpace

for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds

( ( for R being RestFunc of Y holds R * J is RestFunc of (REAL-NS 1),Y ) & ( for L being LinearFunc of Y holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),Y ) )

for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds

( ( for R being RestFunc of Y holds R * J is RestFunc of (REAL-NS 1),Y ) & ( for L being LinearFunc of Y holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),Y ) )

proof end;

theorem FTh42: :: ORDEQ_02:5

for Y being RealNormSpace

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds

( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds

( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

proof end;

theorem FTh43: :: ORDEQ_02:6

for Y being RealNormSpace

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Real

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds

( f is_differentiable_in x0 iff g is_differentiable_in y0 )

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Real

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds

( f is_differentiable_in x0 iff g is_differentiable_in y0 )

proof end;

theorem FTh44: :: ORDEQ_02:7

for Y being RealNormSpace

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_differentiable_in x0 iff g is_differentiable_in y0 )

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_differentiable_in x0 iff g is_differentiable_in y0 )

proof end;

LM519A: for x being Point of (REAL-NS 1) ex z being Real st x = <*z*>

proof end;

theorem FTh42A: :: ORDEQ_02:8

for Y being RealNormSpace

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds

||.(diff (g,y0)).|| = ||.(diff (f,x0)).||

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds

||.(diff (g,y0)).|| = ||.(diff (f,x0)).||

proof end;

theorem LM519B1: :: ORDEQ_02:9

for a, b, z being Real

for p, q, x being Point of (REAL-NS 1) st p = <*a*> & q = <*b*> & x = <*z*> holds

( ( z in ].a,b.[ implies x in ].p,q.[ ) & ( x in ].p,q.[ implies ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) ) ) )

for p, q, x being Point of (REAL-NS 1) st p = <*a*> & q = <*b*> & x = <*z*> holds

( ( z in ].a,b.[ implies x in ].p,q.[ ) & ( x in ].p,q.[ implies ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) ) ) )

proof end;

theorem LM519C1: :: ORDEQ_02:10

for a, b, z being Real

for p, q, x being Point of (REAL-NS 1) st p = <*a*> & q = <*b*> & x = <*z*> holds

( ( z in [.a,b.] implies x in [.p,q.] ) & ( x in [.p,q.] implies ( ( a <= b implies z in [.a,b.] ) & ( a >= b implies z in [.b,a.] ) ) ) )

for p, q, x being Point of (REAL-NS 1) st p = <*a*> & q = <*b*> & x = <*z*> holds

( ( z in [.a,b.] implies x in [.p,q.] ) & ( x in [.p,q.] implies ( ( a <= b implies z in [.a,b.] ) & ( a >= b implies z in [.b,a.] ) ) ) )

proof end;

theorem LM519D: :: ORDEQ_02:11

for a, b being Real

for p, q being Point of (REAL-NS 1)

for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds

( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )

for p, q being Point of (REAL-NS 1)

for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds

( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )

proof end;

theorem Th519: :: ORDEQ_02:12

for Y being RealNormSpace

for g being PartFunc of REAL, the carrier of Y

for a, b, M being Real st a <= b & [.a,b.] c= dom g & ( for x being Real st x in [.a,b.] holds

g is_continuous_in x ) & ( for x being Real st x in ].a,b.[ holds

g is_differentiable_in x ) & ( for x being Real st x in ].a,b.[ holds

||.(diff (g,x)).|| <= M ) holds

||.((g /. b) - (g /. a)).|| <= M * |.(b - a).|

for g being PartFunc of REAL, the carrier of Y

for a, b, M being Real st a <= b & [.a,b.] c= dom g & ( for x being Real st x in [.a,b.] holds

g is_continuous_in x ) & ( for x being Real st x in ].a,b.[ holds

g is_differentiable_in x ) & ( for x being Real st x in ].a,b.[ holds

||.(diff (g,x)).|| <= M ) holds

||.((g /. b) - (g /. a)).|| <= M * |.(b - a).|

proof end;

Lm13a: for Y being RealBanachSpace

for a, b, c, d, e being Real

for f being continuous PartFunc of REAL, the carrier of Y st [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.] & ( for x being Real st x in [.(min (c,d)),(max (c,d)).] holds

||.(f /. x).|| <= e ) holds

||.(integral (f,c,d)).|| <= e * |.(d - c).|

proof end;

Lm14a: for Y being RealBanachSpace

for a, b, c, d, e being Real

for f being continuous PartFunc of REAL, the carrier of Y st c <= d & [.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)

proof end;

Lm17: for a being Real

for X being RealNormSpace

for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / |.a.|

proof end;

theorem Th1955: :: ORDEQ_02:13

for a, b, x0 being Real

for X being RealBanachSpace

for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F /. x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds

( F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

for X being RealBanachSpace

for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F /. x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds

( F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

proof end;

theorem Th35: :: ORDEQ_02:14

for X being RealBanachSpace

for a, b being Real

for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) holds

for x being Real st x in [.a,b.] holds

F is_continuous_in x

for a, b being Real

for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) holds

for x being Real st x in [.a,b.] holds

F is_continuous_in x

proof end;

theorem Lm00: :: ORDEQ_02:15

for X being RealBanachSpace

for a being Real

for f being continuous PartFunc of REAL, the carrier of X st a in dom f holds

integral (f,a,a) = 0. X

for a being Real

for f being continuous PartFunc of REAL, the carrier of X st a in dom f holds

integral (f,a,a) = 0. X

proof end;

theorem Th40a: :: ORDEQ_02:16

for X being RealBanachSpace

for a, b being Real

for y0 being VECTOR of X

for f being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X st a <= b & dom f = [.a,b.] & ( for t being Real st t in [.a,b.] holds

g /. t = y0 + (integral (f,a,t)) ) holds

g /. a = y0

for a, b being Real

for y0 being VECTOR of X

for f being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X st a <= b & dom f = [.a,b.] & ( for t being Real st t in [.a,b.] holds

g /. t = y0 + (integral (f,a,t)) ) holds

g /. a = y0

proof end;

theorem Th40: :: ORDEQ_02:17

for X being RealBanachSpace

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for f being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X st 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 is_differentiable_on Z & ( for t being Real st t in Z holds

diff (g,t) = f /. t ) )

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for f being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X st 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 is_differentiable_on Z & ( for t being Real st t in Z holds

diff (g,t) = f /. t ) )

proof end;

theorem Th45a: :: ORDEQ_02:18

for X being RealBanachSpace

for a, b being Real

for f being PartFunc of REAL, the carrier of X st a <= b & [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) holds

f /. b = f /. a

for a, b being Real

for f being PartFunc of REAL, the carrier of X st a <= b & [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) holds

f /. b = f /. a

proof end;

theorem Th45: :: ORDEQ_02:19

for X being RealBanachSpace

for a, b being Real

for f being PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) holds

f | ].a,b.[ is constant

for a, b being Real

for f being PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds

f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds

diff (f,x) = 0. X ) holds

f | ].a,b.[ is constant

proof end;

theorem Th46: :: ORDEQ_02:20

for X being RealBanachSpace

for a, b being Real

for f being continuous PartFunc of REAL, the carrier of X st [.a,b.] = dom f & f | ].a,b.[ is constant holds

for x being Real st x in [.a,b.] holds

f /. x = f /. a

for a, b being Real

for f being continuous PartFunc of REAL, the carrier of X st [.a,b.] = dom f & f | ].a,b.[ is constant holds

for x being Real st x in [.a,b.] holds

f /. x = f /. a

proof end;

theorem Th47: :: ORDEQ_02:21

for X being RealBanachSpace

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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

proof end;

Lm4: 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) )

proof end;

Lm5: 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

proof end;

Lm6: 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 )

proof end;

Lm7: 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 )

proof end;

definition

let X be RealBanachSpace;

let y0 be VECTOR of X;

let G be Function of X,X;

let a, b be Real;

assume A1: ( a <= b & G is_continuous_on dom G ) ;

ex b_{1} being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) st

for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X st

( x = f & b_{1} . 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 b_{1}, b_{2} being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) st ( for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X st

( x = f & b_{1} . 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'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X st

( x = f & b_{2} . 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

b_{1} = b_{2}

end;
let y0 be VECTOR of X;

let G be Function of X,X;

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'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) means :Def8: :: ORDEQ_02:def 1

for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X 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 for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X 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)) ) );

ex b

for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X st

( x = f & b

g /. t = y0 + (integral (Gf,a,t)) ) )

proof end;

uniqueness for b

( x = f & b

g /. t = y0 + (integral (Gf,a,t)) ) ) ) & ( for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X st

( x = f & b

g /. t = y0 + (integral (Gf,a,t)) ) ) ) holds

b

proof end;

:: deftheorem Def8 defines Fredholm ORDEQ_02:def 1 :

for X being RealBanachSpace

for y0 being VECTOR of X

for G being Function of X,X

for a, b being Real st a <= b & G is_continuous_on dom G holds

for b_{6} being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds

( b_{6} = Fredholm (G,a,b,y0) iff for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X st

( x = f & b_{6} . 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 RealBanachSpace

for y0 being VECTOR of X

for G being Function of X,X

for a, b being Real st a <= b & G is_continuous_on dom G holds

for b

( b

( x = f & b

g /. t = y0 + (integral (Gf,a,t)) ) ) );

theorem Th53: :: ORDEQ_02:22

for X being RealBanachSpace

for a, b, r being Real

for y0 being VECTOR of X

for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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).||

for a, b, r being Real

for y0 being VECTOR of X

for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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).||

proof end;

theorem Th54: :: ORDEQ_02:23

for X being RealBanachSpace

for a, b, r being Real

for y0 being VECTOR of X

for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X 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).||

for a, b, r being Real

for y0 being VECTOR of X

for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X 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).||

proof end;

Lm8: 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

proof end;

Lm9: 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) !) )

proof end;

theorem Th55: :: ORDEQ_02:24

for X being RealBanachSpace

for a, b, r being Real

for y0 being VECTOR of X

for G being Function of X,X

for m being Nat st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) 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).||

for a, b, r being Real

for y0 being VECTOR of X

for G being Function of X,X

for m being Nat st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) 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).||

proof end;

theorem Th56: :: ORDEQ_02:25

for X being RealBanachSpace

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & G is_Lipschitzian_on the carrier of X holds

ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & G is_Lipschitzian_on the carrier of X holds

ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction

proof end;

theorem Th57: :: ORDEQ_02:26

for X being RealBanachSpace

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & G is_Lipschitzian_on the carrier of X holds

Fredholm (G,a,b,y0) is with_unique_fixpoint

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & G is_Lipschitzian_on the carrier of X holds

Fredholm (G,a,b,y0) is with_unique_fixpoint

proof end;

theorem Th58: :: ORDEQ_02:27

for X being RealBanachSpace

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & 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 ) )

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & 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 ) )

proof end;

theorem Th59: :: ORDEQ_02:28

for X being RealBanachSpace

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X

for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X

for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

proof end;

theorem :: ORDEQ_02:29

for X being RealBanachSpace

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X

for y1, y2 being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1 /. a = y0 & ( for t being Real st t in Z holds

diff (y1,t) = G . (y1 /. t) ) & dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2 /. a = y0 & ( for t being Real st t in Z holds

diff (y2,t) = G . (y2 /. t) ) holds

y1 = y2

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X

for y1, y2 being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1 /. a = y0 & ( for t being Real st t in Z holds

diff (y1,t) = G . (y1 /. t) ) & dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2 /. a = y0 & ( for t being Real st t in Z holds

diff (y2,t) = G . (y2 /. t) ) holds

y1 = y2

proof end;

theorem :: ORDEQ_02:30

for X being RealBanachSpace

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

proof end;