:: Contracting Mapping on Normed Linear Space
:: by Keiichi Miyajima , Artur Korni{\l}owicz and Yasunari Shidama
::
:: Copyright (c) 2012-2021 Association of Mizar Users

definition
let f be Function;
attr f is with_unique_fixpoint means :: ORDEQ_01:def 1
ex x being set st
( x is_a_fixpoint_of f & ( for y being set st y is_a_fixpoint_of f holds
x = y ) );
end;

:: deftheorem defines with_unique_fixpoint ORDEQ_01:def 1 :
for f being Function holds
( f is with_unique_fixpoint iff ex x being set st
( x is_a_fixpoint_of f & ( for y being set st y is_a_fixpoint_of f holds
x = y ) ) );

theorem :: ORDEQ_01:1
for x being set holds x is_a_fixpoint_of {[x,x]}
proof end;

theorem Th2: :: ORDEQ_01:2
for x, y, z being set st x is_a_fixpoint_of {[y,z]} holds
x = y
proof end;

registration
let x be set ;
coherence
proof end;
end;

theorem Th3: :: ORDEQ_01:3
for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
< e ) holds
x = 0. X
proof end;

theorem :: ORDEQ_01:4
for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
proof end;

theorem :: ORDEQ_01:5
for K, L, e being Real st 0 < K & K < 1 & 0 < e holds
ex n being Nat st |.(L * (K to_power n)).| < e
proof end;

registration
let X be RealNormSpace;
cluster Function-like V22() quasi_total -> contraction for Element of K16(K17( the carrier of X, the carrier of X));
coherence
for b1 being Function of X,X st b1 is V22() holds
b1 is contraction
proof end;
end;

registration
let X be RealBanachSpace;
cluster Function-like quasi_total contraction -> with_unique_fixpoint for Element of K16(K17( the carrier of X, the carrier of X));
coherence
for b1 being Function of X,X st b1 is contraction holds
b1 is with_unique_fixpoint
proof end;
end;

theorem :: ORDEQ_01:6
canceled;

::\$CT
theorem Th7: :: ORDEQ_01:7
for X being RealBanachSpace
for f being Function of X,X st ex n0 being Nat st iter (f,n0) is contraction holds
f is with_unique_fixpoint
proof end;

theorem :: ORDEQ_01:8
for X being RealBanachSpace
for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is contraction holds
ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
proof end;

theorem Th9: :: ORDEQ_01:9
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being continuous PartFunc of REAL,Y st dom f = X holds
f is bounded Function of X,Y
proof end;

definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func ContinuousFunctions (X,Y) -> Subset of means :Def2: :: ORDEQ_01:def 2
for x being set holds
( x in it iff ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) );
existence
ex b1 being Subset of st
for x being set holds
( x in b1 iff ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) )
proof end;
uniqueness
for b1, b2 being Subset of st ( for x being set holds
( x in b1 iff ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) ) ) & ( for x being set holds
( x in b2 iff ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ContinuousFunctions ORDEQ_01:def 2 :
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for b3 being Subset of holds
( b3 = ContinuousFunctions (X,Y) iff for x being set holds
( x in b3 iff ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) ) );

registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
cluster ContinuousFunctions (X,Y) -> non empty ;
coherence
not ContinuousFunctions (X,Y) is empty
proof end;
end;

registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
coherence
proof end;
end;

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 :: ORDEQ_01:def 3
RLSStruct(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),)),(Add_ ((ContinuousFunctions (X,Y)),)),(Mult_ ((ContinuousFunctions (X,Y)),)) #);
coherence
RLSStruct(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),)),(Add_ ((ContinuousFunctions (X,Y)),)),(Mult_ ((ContinuousFunctions (X,Y)),)) #) is strict RealLinearSpace
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)),)),(Add_ ((ContinuousFunctions (X,Y)),)),(Mult_ ((ContinuousFunctions (X,Y)),)) #);

registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
coherence ;
end;

theorem Th10: :: ORDEQ_01:10
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g, h being VECTOR of
for f9, g9, h9 being continuous PartFunc of REAL,Y st f9 = f & g9 = g & h9 = h & dom f9 = X & dom g9 = X & dom h9 = X holds
( h = f + g iff for x being Element of X holds h9 /. x = (f9 /. x) + (g9 /. x) )
proof end;

theorem Th11: :: ORDEQ_01:11
for a being Real
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, h being VECTOR of
for f9, h9 being continuous PartFunc of REAL,Y st f9 = f & h9 = h & dom f9 = X & dom h9 = X holds
( h = a * f iff for x being Element of X holds h9 /. x = a * (f9 /. x) )
proof end;

theorem Th12: :: ORDEQ_01:12
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds 0. = X --> (0. Y)
proof end;

definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func ContinuousFunctionsNorm (X,Y) -> Function of (ContinuousFunctions (X,Y)),REAL equals :: ORDEQ_01:def 4
(BoundedFunctionsNorm (X,Y)) | (ContinuousFunctions (X,Y));
correctness
coherence
(BoundedFunctionsNorm (X,Y)) | (ContinuousFunctions (X,Y)) is Function of (ContinuousFunctions (X,Y)),REAL
;
by FUNCT_2:32;
end;

:: deftheorem defines ContinuousFunctionsNorm ORDEQ_01:def 4 :
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds ContinuousFunctionsNorm (X,Y) = (BoundedFunctionsNorm (X,Y)) | (ContinuousFunctions (X,Y));

definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let f be set ;
assume A1: f in ContinuousFunctions (X,Y) ;
func modetrans (f,X,Y) -> continuous PartFunc of REAL,Y means :Def5: :: ORDEQ_01:def 5
( it = f & dom it = X );
correctness
existence
ex b1 being continuous PartFunc of REAL,Y st
( b1 = f & dom b1 = X )
;
uniqueness
for b1, b2 being continuous PartFunc of REAL,Y st b1 = f & dom b1 = X & b2 = f & dom b2 = X holds
b1 = b2
;
by ;
end;

:: deftheorem Def5 defines modetrans ORDEQ_01:def 5 :
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being set st f in ContinuousFunctions (X,Y) holds
for b4 being continuous PartFunc of REAL,Y holds
( b4 = modetrans (f,X,Y) iff ( b4 = f & dom b4 = X ) );

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 :: ORDEQ_01:def 6
NORMSTR(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),)),(Add_ ((ContinuousFunctions (X,Y)),)),(Mult_ ((ContinuousFunctions (X,Y)),)),() #);
coherence
NORMSTR(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),)),(Add_ ((ContinuousFunctions (X,Y)),)),(Mult_ ((ContinuousFunctions (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)),)),(Add_ ((ContinuousFunctions (X,Y)),)),(Mult_ ((ContinuousFunctions (X,Y)),)),() #);

theorem :: ORDEQ_01:13
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being continuous PartFunc of REAL,Y st dom f = X holds
modetrans (f,X,Y) = f
proof end;

theorem Th14: :: ORDEQ_01:14
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds X --> (0. Y) = 0.
proof end;

theorem Th15: :: ORDEQ_01:15
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g, h being Point of
for f9, g9, h9 being continuous PartFunc of REAL,Y st f9 = f & g9 = g & h9 = h & dom f9 = X & dom g9 = X & dom h9 = X holds
( h = f + g iff for x being Element of X holds h9 /. x = (f9 /. x) + (g9 /. x) )
proof end;

theorem :: ORDEQ_01:16
for a being Real
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, h being Point of
for f9, h9 being continuous PartFunc of REAL,Y st f9 = f & h9 = h & dom f9 = X & dom h9 = X holds
( h = a * f iff for x being Element of X holds h9 /. x = a * (f9 /. x) )
proof end;

theorem Th17: :: ORDEQ_01:17
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being Point of
for g being Point of () st f = g holds
= by FUNCT_1:49;

theorem Th18: :: ORDEQ_01:18
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g being Point of
for f1, g1 being Point of () st f1 = f & g1 = g holds
f + g = f1 + g1
proof end;

theorem Th19: :: ORDEQ_01:19
for a being Real
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being Point of
for f1 being Point of () st f1 = f holds
a * f = a * f1
proof end;

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 holds
( ( = 0 implies f = 0. ) & ( f = 0. implies = 0 ) & ||.(a * f).|| = |.a.| * & ||.(f + g).|| <= + )

proof end;

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 )

proof end;

Lm4: for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace

proof end;

registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
coherence by Lm4;
end;

theorem Th20: :: ORDEQ_01:20
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g, h being Point of
for f9, g9, h9 being continuous PartFunc of REAL,Y st f9 = f & g9 = g & h9 = h & dom f9 = X & dom g9 = X & dom h9 = X holds
( h = f - g iff for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) )
proof end;

theorem Th21: :: ORDEQ_01:21
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g being Point of
for f1, g1 being Point of () st f1 = f & g1 = g holds
f - g = f1 - g1
proof end;

Lm5: for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for C being Subset of () st C = ContinuousFunctions (X,Y) holds
C is closed

proof end;

registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
cluster closed for Element of K16( the carrier of ());
existence
ex b1 being Subset of () st b1 is closed
proof end;
end;

theorem Th22: :: ORDEQ_01:22
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds ContinuousFunctions (X,Y) is closed Subset of () by Lm5;

theorem Th23: :: ORDEQ_01:23
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for seq being sequence of st Y is complete & seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof end;

Lm6: for X being non empty closed_interval Subset of REAL
for Y being RealBanachSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) is RealBanachSpace

proof end;

registration
let X be non empty closed_interval Subset of REAL;
let Y be RealBanachSpace;
coherence by Lm6;
end;

theorem Th24: :: ORDEQ_01:24
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for v being Point of
for g being PartFunc of REAL,Y st g = v holds
for t being Real st t in X holds
||.(g /. t).|| <=
proof end;

theorem Th25: :: ORDEQ_01:25
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for K being Real
for v being Point of
for g being PartFunc of REAL,Y st g = v & ( for t being Real st t in X holds
||.(g /. t).|| <= K ) holds
<= K
proof end;

theorem Th26: :: ORDEQ_01:26
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for v1, v2 being Point of
for g1, g2 being PartFunc of REAL,Y st g1 = v1 & g2 = v2 holds
for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).||
proof end;

theorem Th27: :: ORDEQ_01:27
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for K being Real
for v1, v2 being Point of
for g1, g2 being PartFunc of REAL,Y st g1 = v1 & g2 = v2 & ( for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= K ) holds
||.(v1 - v2).|| <= K
proof end;

theorem Th28: :: ORDEQ_01:28
for n, i being Nat
for f being PartFunc of REAL,(REAL n)
for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
proof end;

theorem Th29: :: ORDEQ_01:29
for n being non zero Element of NAT
for a, b being Real
for g being continuous PartFunc of REAL,(REAL n) st dom g = ['a,b'] holds
g | ['a,b'] is bounded
proof end;

theorem Th30: :: ORDEQ_01:30
for n being non zero Element of NAT
for a, b being Real
for g being continuous PartFunc of REAL,(REAL n) st dom g = ['a,b'] holds
g is_integrable_on ['a,b']
proof end;

theorem Th31: :: ORDEQ_01:31
for n being non zero Element of NAT
for a, b being Real
for f, F being PartFunc of REAL,(REAL n) st a <= b & dom f = ['a,b'] & dom F = ['a,b'] & f is continuous & ( 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 Th32: :: ORDEQ_01:32
for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,() st dom f = ['a,b'] holds
f | ['a,b'] is bounded
proof end;

theorem Th33: :: ORDEQ_01:33
for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,() st dom f = ['a,b'] holds
f is_integrable_on ['a,b']
proof end;

theorem Th34: :: ORDEQ_01:34
for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,()
for F being PartFunc of REAL,() st a <= b & 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 Th35: :: ORDEQ_01:35
for R being PartFunc of REAL,REAL st R is total holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
() * |.(R /. z).| < r ) ) )
proof end;

theorem Th36: :: ORDEQ_01:36
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 ()
for f being continuous PartFunc of REAL,()
for g being PartFunc of REAL,() 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 ) )
proof end;

theorem :: ORDEQ_01:37
for n being non zero Element of NAT
for i being Nat
for y1, y2 being Point of () holds (proj (i,n)) . (y1 + y2) = ((proj (i,n)) . y1) + ((proj (i,n)) . y2)
proof end;

theorem Th38: :: ORDEQ_01:38
for n being non zero Element of NAT
for i being Nat
for y1 being Point of ()
for r being Real holds (proj (i,n)) . (r * y1) = r * ((proj (i,n)) . y1)
proof end;

theorem Th39: :: ORDEQ_01:39
for n being non zero Element of NAT
for g being PartFunc of REAL,()
for x0 being Real
for i being Nat st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (proj (i,n)) * g is_differentiable_in x0 & (proj (i,n)) . (diff (g,x0)) = diff (((proj (i,n)) * g),x0) )
proof end;

Lm7: for n being non zero Element of NAT
for i being Nat holds (proj (i,n)) . (0. ()) = 0

proof end;

theorem Th40: :: ORDEQ_01:40
for n being non zero Element of NAT
for f being PartFunc of REAL,()
for X being set st ( for i being Nat st 1 <= i & i <= n holds
((proj (i,n)) * f) | X is V22() ) holds
f | X is V22()
proof end;

theorem Th41: :: ORDEQ_01:41
for n being non zero Element of NAT
for a, b being Real
for f being PartFunc of REAL,() st ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (f,x) = 0. () ) holds
f | ].a,b.[ is V22()
proof end;

theorem Th42: :: ORDEQ_01:42
for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,() st a < b & [.a,b.] = dom f & f | ].a,b.[ is V22() holds
for x being Real st x in [.a,b.] holds
f . x = f . a
proof end;

theorem Th43: :: ORDEQ_01:43
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 ()
for y, Gf being continuous PartFunc of REAL,()
for g being PartFunc of REAL,() 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;

theorem Th44: :: ORDEQ_01:44
for n being non zero Element of NAT
for a, b, c, d being Real
for f being PartFunc of REAL,() st a <= b & f is_integrable_on ['a,b'] & is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( is_integrable_on ['(min (c,d)),(max (c,d))'] & | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (,(min (c,d)),(max (c,d))) )
proof end;

theorem Th45: :: ORDEQ_01:45
for n being non zero Element of NAT
for a, b, c, d, e being Real
for f being PartFunc of REAL,() st a <= b & c <= d & f is_integrable_on ['a,b'] & 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) )
proof end;

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 )

proof end;

theorem Th46: :: ORDEQ_01:46
for a being Real
for n being Nat
for g being Function of REAL,REAL st ( for x being Real holds g . x = (x - a) |^ (n + 1) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = (n + 1) * ((x - a) |^ n) )
proof end;

theorem Th47: :: ORDEQ_01:47
for a being Real
for n being Nat
for g being Function of REAL,REAL st ( for x being Real holds g . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) )
proof end;

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

proof end;

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

proof end;

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 )

proof end;

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 )

proof end;

theorem Th48: :: ORDEQ_01:48
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)
proof end;

definition
let n be non zero Element of NAT ;
let y0 be VECTOR of ();
let G be Function of (),();
let a, b be Real;
assume A1: ( a <= b & G is_continuous_on dom G ) ;
func Fredholm (G,a,b,y0) -> Function of (),() means :Def7: :: ORDEQ_01:def 7
for x being VECTOR of () ex f, g, Gf being continuous PartFunc of REAL,() 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 (),() st
for x being VECTOR of () ex f, g, Gf being continuous PartFunc of REAL,() 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)) ) )
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for x being VECTOR of () ex f, g, Gf being continuous PartFunc of REAL,() 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 () ex f, g, Gf being continuous PartFunc of REAL,() 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
proof end;
end;

:: deftheorem Def7 defines Fredholm ORDEQ_01:def 7 :
for n being non zero Element of NAT
for y0 being VECTOR of ()
for G being Function of (),()
for a, b being Real st a <= b & G is_continuous_on dom G holds
for b6 being Function of (),() holds
( b6 = Fredholm (G,a,b,y0) iff for x being VECTOR of () ex f, g, Gf being continuous PartFunc of REAL,() 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: :: ORDEQ_01:49
for n being non zero Element of NAT
for a, b, r being Real
for y0 being VECTOR of ()
for G being Function of (),() st a <= b & 0 < r & ( for y1, y2 being VECTOR of () holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of ()
for g, h being continuous PartFunc of REAL,() 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 Th50: :: ORDEQ_01:50
for n being non zero Element of NAT
for a, b, r being Real
for y0 being VECTOR of ()
for G being Function of (),() st a <= b & 0 < r & ( for y1, y2 being VECTOR of () holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of ()
for m being Element of NAT
for g, h being continuous PartFunc of REAL,() 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;

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

proof end;

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

proof end;

theorem Th51: :: ORDEQ_01:51
for n being non zero Element of NAT
for a, b, r being Real
for y0 being VECTOR of ()
for G being Function of (),()
for m being Nat st a <= b & 0 < r & ( for y1, y2 being VECTOR of () holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of () 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 Th52: :: ORDEQ_01:52
for n being non zero Element of NAT
for a, b being Real
for y0 being VECTOR of ()
for G being Function of (),() st a < b & G is_Lipschitzian_on the carrier of () holds
ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction
proof end;

theorem Th53: :: ORDEQ_01:53
for n being non zero Element of NAT
for a, b being Real
for y0 being VECTOR of ()
for G being Function of (),() st a < b & G is_Lipschitzian_on the carrier of () holds
Fredholm (G,a,b,y0) is with_unique_fixpoint
proof end;

theorem Th54: :: ORDEQ_01:54
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 ()
for G being Function of (),()
for f, g being continuous PartFunc of REAL,() st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of () & 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 Th55: :: ORDEQ_01:55
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 ()
for G being Function of (),()
for y being continuous PartFunc of REAL,() st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of () & 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_01:56
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 ()
for G being Function of (),()
for y1, y2 being continuous PartFunc of REAL,() st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of () & 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_01:57
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 ()
for G being Function of (),() st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of () holds
ex y being continuous PartFunc of REAL,() 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;