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)); :: thesis: 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;
now :: thesis: for x0 being Real st x0 in dom (G * f0) holds
G * f0 is_continuous_in x0
let x0 be Real; :: thesis: ( x0 in dom (G * f0) implies G * f0 is_continuous_in x0 )
assume A4: x0 in dom (G * f0) ; :: thesis: G * f0 is_continuous_in x0
then f0 is_continuous_in x0 by NFCONT_3:def 2, FUNCT_1:11;
hence G * f0 is_continuous_in x0 by A4, X1, NFCONT_3:15, A1; :: thesis: verum
end;
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 :: thesis: for t being Real st t in [.a,b.] holds
(F0 | ['a,b']) /. t = integral (Gf,a,t)
let t be Real; :: thesis: ( t in [.a,b.] implies (F0 | ['a,b']) /. t = integral (Gf,a,t) )
assume A11: t in [.a,b.] ; :: thesis: (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 ; :: thesis: 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 :: thesis: for t being Real st t in [.a,b.] holds
((REAL --> y0) | ['a,b']) /. t = y0
let t be Real; :: thesis: ( t in [.a,b.] implies ((REAL --> y0) | ['a,b']) /. t = y0 )
assume A16: t in [.a,b.] ; :: thesis: ((REAL --> y0) | ['a,b']) /. t = y0
hence ((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 ;
:: thesis: 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 ; :: thesis: S1[x,y]
now :: thesis: for t being Real st t in ['a,b'] holds
g /. t = y0 + (integral (Gf,a,t))
let t be Real; :: thesis: ( t in ['a,b'] implies g /. t = y0 + (integral (Gf,a,t)) )
assume A20: t in ['a,b'] ; :: thesis: 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; :: thesis: verum
end;
hence S1[x,y] by A19, A3; :: thesis: 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 ; :: thesis: 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; :: thesis: verum