defpred S1[ set , set ] means ex f, g, Gf being continuous PartFunc of REAL,(REAL-NS n) 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'],(REAL-NS n)));
A2:
for x being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ex y being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) st S1[x,y]
proof
let x be
Element of the
carrier of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n)));
ex y being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) st S1[x,y]
consider f0 being
continuous PartFunc of
REAL,
(REAL-NS n) such that A3:
(
x = f0 &
dom f0 = ['a,b'] )
by Def2;
then reconsider Gf =
G * f0 as
continuous PartFunc of
REAL,
(REAL-NS n) by NFCONT_3:def 2;
dom G = the
carrier of
(REAL-NS n)
by FUNCT_2:def 1;
then
rng f0 c= dom G
;
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
(REAL-NS n) =
integral (
Gf,
a,$1);
consider F0 being
Function of
REAL,
(REAL-NS n) such that A8:
for
x being
Element of
REAL holds
F0 . x = H1(
x)
from FUNCT_2:sch 4();
set F =
F0 | ['a,b'];
A9:
dom (F0 | ['a,b']) =
(dom F0) /\ ['a,b']
by RELAT_1:61
.=
REAL /\ ['a,b']
by FUNCT_2:def 1
.=
['a,b']
by XBOOLE_1:28
;
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 . t
by A11, A9, A7, FUNCT_1:47
.=
integral (
Gf,
a,
t)
by A8, A12
;
verum end;
A13:
for
t being
Real st
t in [.a,b.] holds
F0 | ['a,b'] is_continuous_in t
by Th34, A6, A1, A9, A10;
set G0 =
REAL --> y0;
set G1 =
(REAL --> y0) | ['a,b'];
A14:
dom ((REAL --> y0) | ['a,b']) =
(dom (REAL --> y0)) /\ ['a,b']
by RELAT_1:61
.=
REAL /\ ['a,b']
.=
['a,b']
by XBOOLE_1:28
;
A17:
F0 | ['a,b'] is
continuous
by A7, A9, A13, NFCONT_3:def 2;
set g =
((REAL --> y0) | ['a,b']) + (F0 | ['a,b']);
A18:
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
;
reconsider g =
((REAL --> y0) | ['a,b']) + (F0 | ['a,b']) as
continuous PartFunc of
REAL,
(REAL-NS n) by A17;
reconsider y =
g as
Element of the
carrier of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) by A18, Def2;
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 A19:
t in ['a,b']
;
g . t = y0 + (integral (Gf,a,t))A20:
((REAL --> y0) | ['a,b']) /. t =
((REAL --> y0) | ['a,b']) . t
by A19, A14, PARTFUN1:def 6
.=
y0
by A19, A7, A15
;
A21:
(F0 | ['a,b']) /. t =
(F0 | ['a,b']) . t
by A19, A9, PARTFUN1:def 6
.=
integral (
Gf,
a,
t)
by A19, A7, A10
;
thus g . t =
g /. t
by A18, A19, PARTFUN1:def 6
.=
y0 + (integral (Gf,a,t))
by A20, A21, A18, A19, VFUNCT_1:def 1
;
verum end;
hence
S1[
x,
y]
by A18, A3;
verum
end;
consider F being Function of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))), the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) such that
A22:
for x being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) holds S1[x,F . x]
from FUNCT_2:sch 3(A2);
take
F
; 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 & 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'],(REAL-NS n))) ex f, g, Gf being continuous PartFunc of REAL,(REAL-NS n) 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 A22; verum