:: by Keiichi Miyajima , Artur Korni{\l}owicz and Yasunari Shidama

::

:: Received August 19, 2012

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

definition

let f be Function;

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

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

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

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 Th3: :: ORDEQ_01:3

for X being RealNormSpace

for x being Point of X st ( for e being Real st e > 0 holds

||.x.|| < e ) holds

x = 0. X

for x being Point of X st ( for e being Real st e > 0 holds

||.x.|| < 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

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

ex n being Nat st |.(L * (K to_power n)).| < e

proof end;

registration

let X be RealNormSpace;

coherence

for b_{1} being Function of X,X st b_{1} is V22() holds

b_{1} is contraction

end;
coherence

for b

b

proof end;

registration

let X be RealBanachSpace;

coherence

for b_{1} being Function of X,X st b_{1} is contraction holds

b_{1} is with_unique_fixpoint

end;
coherence

for b

b

proof end;

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

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

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

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;

ex b_{1} being Subset of (R_VectorSpace_of_BoundedFunctions (X,Y)) st

for x being set holds

( x in b_{1} iff ex f being continuous PartFunc of REAL,Y st

( x = f & dom f = X ) )

for b_{1}, b_{2} being Subset of (R_VectorSpace_of_BoundedFunctions (X,Y)) st ( for x being set holds

( x in b_{1} iff ex f being continuous PartFunc of REAL,Y st

( x = f & dom f = X ) ) ) & ( for x being set holds

( x in b_{2} iff ex f being continuous PartFunc of REAL,Y st

( x = f & dom f = X ) ) ) holds

b_{1} = b_{2}

end;
let Y be RealNormSpace;

func ContinuousFunctions (X,Y) -> Subset of (R_VectorSpace_of_BoundedFunctions (X,Y)) 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 for x being set holds

( x in it iff ex f being continuous PartFunc of REAL,Y st

( x = f & dom f = X ) );

ex b

for x being set holds

( x in b

( x = f & dom f = X ) )

proof end;

uniqueness for b

( x in b

( x = f & dom f = X ) ) ) & ( for x being set holds

( x in b

( x = f & dom f = X ) ) ) holds

b

proof end;

:: deftheorem Def2 defines ContinuousFunctions ORDEQ_01:def 2 :

for X being non empty closed_interval Subset of REAL

for Y being RealNormSpace

for b_{3} being Subset of (R_VectorSpace_of_BoundedFunctions (X,Y)) holds

( b_{3} = ContinuousFunctions (X,Y) iff for x being set holds

( x in b_{3} iff ex f being continuous PartFunc of REAL,Y st

( x = f & dom f = X ) ) );

for X being non empty closed_interval Subset of REAL

for Y being RealNormSpace

for b

( b

( x in b

( x = f & dom f = X ) ) );

registration

let X be non empty closed_interval Subset of REAL;

let Y be RealNormSpace;

coherence

not ContinuousFunctions (X,Y) is empty

end;
let Y be RealNormSpace;

coherence

not ContinuousFunctions (X,Y) is empty

proof end;

registration

let X be non empty closed_interval Subset of REAL;

let Y be RealNormSpace;

coherence

ContinuousFunctions (X,Y) is linearly-closed

end;
let Y be RealNormSpace;

coherence

ContinuousFunctions (X,Y) is linearly-closed

proof end;

definition

let X be non empty closed_interval Subset of REAL;

let Y be RealNormSpace;

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;
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)),(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)))) #);

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;

:: 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)))) #);

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

registration

let X be non empty closed_interval Subset of REAL;

let Y be RealNormSpace;

coherence

( R_VectorSpace_of_ContinuousFunctions (X,Y) is Abelian & R_VectorSpace_of_ContinuousFunctions (X,Y) is add-associative & R_VectorSpace_of_ContinuousFunctions (X,Y) is right_zeroed & R_VectorSpace_of_ContinuousFunctions (X,Y) is right_complementable & R_VectorSpace_of_ContinuousFunctions (X,Y) is vector-distributive & R_VectorSpace_of_ContinuousFunctions (X,Y) is scalar-distributive & R_VectorSpace_of_ContinuousFunctions (X,Y) is scalar-associative & R_VectorSpace_of_ContinuousFunctions (X,Y) is scalar-unital ) ;

end;
let Y be RealNormSpace;

coherence

( R_VectorSpace_of_ContinuousFunctions (X,Y) is Abelian & R_VectorSpace_of_ContinuousFunctions (X,Y) is add-associative & R_VectorSpace_of_ContinuousFunctions (X,Y) is right_zeroed & R_VectorSpace_of_ContinuousFunctions (X,Y) is right_complementable & R_VectorSpace_of_ContinuousFunctions (X,Y) is vector-distributive & R_VectorSpace_of_ContinuousFunctions (X,Y) is scalar-distributive & R_VectorSpace_of_ContinuousFunctions (X,Y) is scalar-associative & R_VectorSpace_of_ContinuousFunctions (X,Y) is scalar-unital ) ;

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 (R_VectorSpace_of_ContinuousFunctions (X,Y))

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

for Y being RealNormSpace

for f, g, h being VECTOR of (R_VectorSpace_of_ContinuousFunctions (X,Y))

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 (R_VectorSpace_of_ContinuousFunctions (X,Y))

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

for X being non empty closed_interval Subset of REAL

for Y being RealNormSpace

for f, h being VECTOR of (R_VectorSpace_of_ContinuousFunctions (X,Y))

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. (R_VectorSpace_of_ContinuousFunctions (X,Y)) = X --> (0. Y)

for Y being RealNormSpace holds 0. (R_VectorSpace_of_ContinuousFunctions (X,Y)) = X --> (0. Y)

proof end;

definition

let X be non empty closed_interval Subset of REAL;

let Y be RealNormSpace;

coherence

(BoundedFunctionsNorm (X,Y)) | (ContinuousFunctions (X,Y)) is Function of (ContinuousFunctions (X,Y)),REAL;

by FUNCT_2:32;

end;
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 (BoundedFunctionsNorm (X,Y)) | (ContinuousFunctions (X,Y));

coherence

(BoundedFunctionsNorm (X,Y)) | (ContinuousFunctions (X,Y)) is Function of (ContinuousFunctions (X,Y)),REAL;

by FUNCT_2:32;

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

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

existence

ex b_{1} being continuous PartFunc of REAL,Y st

( b_{1} = f & dom b_{1} = X );

uniqueness

for b_{1}, b_{2} being continuous PartFunc of REAL,Y st b_{1} = f & dom b_{1} = X & b_{2} = f & dom b_{2} = X holds

b_{1} = b_{2};

by A1, Def2;

end;
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 ( it = f & dom it = X );

existence

ex b

( b

uniqueness

for b

b

by A1, Def2;

:: 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 b_{4} being continuous PartFunc of REAL,Y holds

( b_{4} = modetrans (f,X,Y) iff ( b_{4} = f & dom b_{4} = X ) );

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 b

( b

definition

let X be non empty closed_interval Subset of REAL;

let Y be RealNormSpace;

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;
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)),(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)) #);

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 ;

:: 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)) #);

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

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

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. (R_NormSpace_of_ContinuousFunctions (X,Y))

for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_ContinuousFunctions (X,Y))

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 (R_NormSpace_of_ContinuousFunctions (X,Y))

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

for Y being RealNormSpace

for f, g, h being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

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 (R_NormSpace_of_ContinuousFunctions (X,Y))

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

for X being non empty closed_interval Subset of REAL

for Y being RealNormSpace

for f, h being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

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 (R_NormSpace_of_ContinuousFunctions (X,Y))

for g being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f = g holds

||.f.|| = ||.g.|| by FUNCT_1:49;

for Y being RealNormSpace

for f being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

for g being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f = g holds

||.f.|| = ||.g.|| 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 (R_NormSpace_of_ContinuousFunctions (X,Y))

for f1, g1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f & g1 = g holds

f + g = f1 + g1

for Y being RealNormSpace

for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

for f1, g1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) 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 (R_NormSpace_of_ContinuousFunctions (X,Y))

for f1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f holds

a * f = a * f1

for X being non empty closed_interval Subset of REAL

for Y being RealNormSpace

for f being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

for f1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) 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 (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.|| )

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;

( 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;
let Y be RealNormSpace;

cluster R_NormSpace_of_ContinuousFunctions (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ;

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;

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 (R_NormSpace_of_ContinuousFunctions (X,Y))

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

for Y being RealNormSpace

for f, g, h being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

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 (R_NormSpace_of_ContinuousFunctions (X,Y))

for f1, g1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f & g1 = g holds

f - g = f1 - g1

for Y being RealNormSpace

for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

for f1, g1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) 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 (R_NormSpace_of_BoundedFunctions (X,Y)) 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;

existence

ex b_{1} being Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) st b_{1} is closed

end;
let Y be RealNormSpace;

existence

ex b

proof 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 (R_NormSpace_of_BoundedFunctions (X,Y)) by Lm5;

for Y being RealNormSpace holds ContinuousFunctions (X,Y) is closed Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) 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 (R_NormSpace_of_ContinuousFunctions (X,Y)) st Y is complete & seq is Cauchy_sequence_by_Norm holds

seq is convergent

for Y being RealNormSpace

for seq being sequence of (R_NormSpace_of_ContinuousFunctions (X,Y)) 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

R_NormSpace_of_ContinuousFunctions (X,Y) is complete by Lm6;

end;
let Y be RealBanachSpace;

coherence

R_NormSpace_of_ContinuousFunctions (X,Y) is complete by Lm6;

theorem Th24: :: ORDEQ_01:24

for X being non empty closed_interval Subset of REAL

for Y being RealNormSpace

for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

for g being PartFunc of REAL,Y st g = v holds

for t being Real st t in X holds

||.(g /. t).|| <= ||.v.||

for Y being RealNormSpace

for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

for g being PartFunc of REAL,Y st g = v holds

for t being Real st t in X holds

||.(g /. t).|| <= ||.v.||

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 (R_NormSpace_of_ContinuousFunctions (X,Y))

for g being PartFunc of REAL,Y st g = v & ( for t being Real st t in X holds

||.(g /. t).|| <= K ) holds

||.v.|| <= K

for Y being RealNormSpace

for K being Real

for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

for g being PartFunc of REAL,Y st g = v & ( for t being Real st t in X holds

||.(g /. t).|| <= K ) holds

||.v.|| <= 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 (R_NormSpace_of_ContinuousFunctions (X,Y))

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

for Y being RealNormSpace

for v1, v2 being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

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 (R_NormSpace_of_ContinuousFunctions (X,Y))

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

for Y being RealNormSpace

for K being Real

for v1, v2 being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))

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

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

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']

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

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,(REAL-NS n) st dom f = ['a,b'] holds

f | ['a,b'] is bounded

for a, b being Real

for f being continuous PartFunc of REAL,(REAL-NS n) 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,(REAL-NS n) st dom f = ['a,b'] holds

f is_integrable_on ['a,b']

for a, b being Real

for f being continuous PartFunc of REAL,(REAL-NS n) 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,(REAL-NS n)

for F being PartFunc of REAL,(REAL-NS n) 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

for a, b being Real

for f being continuous PartFunc of REAL,(REAL-NS n)

for F being PartFunc of REAL,(REAL-NS n) 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

(|.z.| ") * |.(R /. z).| < r ) ) )

( 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

(|.z.| ") * |.(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 (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 ) )

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

proof end;

theorem :: ORDEQ_01:37

for n being non zero Element of NAT

for i being Nat

for y1, y2 being Point of (REAL-NS n) holds (proj (i,n)) . (y1 + y2) = ((proj (i,n)) . y1) + ((proj (i,n)) . y2)

for i being Nat

for y1, y2 being Point of (REAL-NS n) 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 (REAL-NS n)

for r being Real holds (proj (i,n)) . (r * y1) = r * ((proj (i,n)) . y1)

for i being Nat

for y1 being Point of (REAL-NS n)

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,(REAL-NS n)

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

for g being PartFunc of REAL,(REAL-NS n)

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. (REAL-NS n)) = 0

proof end;

theorem Th40: :: ORDEQ_01:40

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL-NS n)

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

for f being PartFunc of REAL,(REAL-NS n)

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,(REAL-NS n) 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. (REAL-NS n) ) holds

f | ].a,b.[ is V22()

for a, b being Real

for f being PartFunc of REAL,(REAL-NS n) 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. (REAL-NS n) ) 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,(REAL-NS n) 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

for a, b being Real

for f being continuous PartFunc of REAL,(REAL-NS n) 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 (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

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

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

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

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

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

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

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

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)

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

ex b_{1} 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 & 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'],(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 & 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'],(REAL-NS n))) ex f, g, Gf being continuous PartFunc of REAL,(REAL-NS n) 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 (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: :: ORDEQ_01:def 7

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

ex b

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 & 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'],(REAL-NS n))) ex f, g, Gf being continuous PartFunc of REAL,(REAL-NS n) st

( x = f & b

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

b

proof 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 b_{6} being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))),(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) holds

( b_{6} = 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 & 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 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 b

( b

( x = f & b

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

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

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

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

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

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

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 (REAL-NS n)

for G being Function of (REAL-NS n),(REAL-NS n) st a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) 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 (REAL-NS n)

for G being Function of (REAL-NS n),(REAL-NS n) st a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) 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 (REAL-NS n)

for G being Function of (REAL-NS n),(REAL-NS n) st a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) holds

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

for a, b being Real

for y0 being VECTOR of (REAL-NS n)

for G being Function of (REAL-NS n),(REAL-NS n) st a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) 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 (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 ) )

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

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 (REAL-NS n)

for G being Function of (REAL-NS n),(REAL-NS n)

for y being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 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 y being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 (REAL-NS n)

for G being Function of (REAL-NS n),(REAL-NS n)

for y1, y2 being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 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 y1, y2 being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 (REAL-NS n)

for G being Function of (REAL-NS n),(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) holds

ex y being continuous PartFunc of REAL,(REAL-NS n) 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 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) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) holds

ex y being continuous PartFunc of REAL,(REAL-NS n) 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;