defpred S1[ set , set ] means ex f, g, Gf being continuous PartFunc of REAL, the carrier of X st
( $1 = f & $2 = 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)) ) );
set D = the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X));
X1:
the carrier of X = dom G
by FUNCT_2:def 1;
A2:
for x being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex y being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) st S1[x,y]
proof
let x be
Element of the
carrier of
(R_NormSpace_of_ContinuousFunctions (['a,b'],X));
ex y being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) st S1[x,y]
consider f0 being
continuous PartFunc of
REAL, the
carrier of
X such that A3:
(
x = f0 &
dom f0 = ['a,b'] )
by ORDEQ_01:def 2;
then reconsider Gf =
G * f0 as
continuous PartFunc of
REAL, the
carrier of
X by NFCONT_3:def 2;
rng f0 c= dom G
by X1;
then A6:
dom Gf = ['a,b']
by A3, RELAT_1:27;
A7:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
deffunc H1(
Element of
REAL )
-> Element of the
carrier of
X =
integral (
Gf,
a,$1);
consider F0 being
Function of
REAL, the
carrier of
X such that A8:
for
x being
Element of
REAL holds
F0 . x = H1(
x)
from FUNCT_2:sch 4();
set F =
F0 | ['a,b'];
dom F0 = REAL
by FUNCT_2:def 1;
then A9:
dom (F0 | ['a,b']) = ['a,b']
by RELAT_1:62;
A10:
now for t being Real st t in [.a,b.] holds
(F0 | ['a,b']) /. t = integral (Gf,a,t)let t be
Real;
( t in [.a,b.] implies (F0 | ['a,b']) /. t = integral (Gf,a,t) )assume A11:
t in [.a,b.]
;
(F0 | ['a,b']) /. t = integral (Gf,a,t)A12:
t in REAL
by XREAL_0:def 1;
thus (F0 | ['a,b']) /. t =
(F0 | ['a,b']) . t
by A7, A9, A11, PARTFUN1:def 6
.=
F0 . t
by A11, A9, A7, FUNCT_1:47
.=
integral (
Gf,
a,
t)
by A8, A12
;
verum end;
set G0 =
REAL --> y0;
set G1 =
(REAL --> y0) | ['a,b'];
dom (REAL --> y0) = REAL
;
then A14:
dom ((REAL --> y0) | ['a,b']) = ['a,b']
by RELAT_1:62;
A15:
now for t being Real st t in [.a,b.] holds
((REAL --> y0) | ['a,b']) /. t = y0let t be
Real;
( t in [.a,b.] implies ((REAL --> y0) | ['a,b']) /. t = y0 )assume A16:
t in [.a,b.]
;
((REAL --> y0) | ['a,b']) /. t = y0hence ((REAL --> y0) | ['a,b']) /. t =
((REAL --> y0) | ['a,b']) . t
by A7, A14, PARTFUN1:def 6
.=
(REAL --> y0) . t
by A16, A14, A7, FUNCT_1:47
.=
y0
by XREAL_0:def 1, FUNCOP_1:7
;
verum end;
set g =
((REAL --> y0) | ['a,b']) + (F0 | ['a,b']);
A19:
dom (((REAL --> y0) | ['a,b']) + (F0 | ['a,b'])) =
(dom (F0 | ['a,b'])) /\ (dom ((REAL --> y0) | ['a,b']))
by VFUNCT_1:def 1
.=
['a,b']
by A9, A14
;
F0 | ['a,b'] is
continuous
by A7, A9, Th35, A6, A10;
then reconsider g =
((REAL --> y0) | ['a,b']) + (F0 | ['a,b']) as
continuous PartFunc of
REAL, the
carrier of
X ;
reconsider y =
g as
Element of the
carrier of
(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) by A19, ORDEQ_01:def 2;
take
y
;
S1[x,y]
now for t being Real st t in ['a,b'] holds
g /. t = y0 + (integral (Gf,a,t))let t be
Real;
( t in ['a,b'] implies g /. t = y0 + (integral (Gf,a,t)) )assume A20:
t in ['a,b']
;
g /. t = y0 + (integral (Gf,a,t))then
(
((REAL --> y0) | ['a,b']) /. t = y0 &
(F0 | ['a,b']) /. t = integral (
Gf,
a,
t) )
by A7, A10, A15;
hence
g /. t = y0 + (integral (Gf,a,t))
by A19, A20, VFUNCT_1:def 1;
verum end;
hence
S1[
x,
y]
by A19, A3;
verum
end;
consider F being Function of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)), the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) such that
A23:
for x being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds S1[x,F . x]
from FUNCT_2:sch 3(A2);
take
F
; 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 & F . 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)) ) )
thus
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 & F . 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)) ) )
by A23; verum