defpred S₁[ 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 S₁[x,y]

proof

let x be Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))); :: thesis: ex y being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) st S₁[x,y]
consider f0 being continuous PartFunc of REAL,(REAL-NS n) such that
A3: ( x = f0 & dom f0 = ['a,b'] ) by Def2;

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 x0 in dom f0 by FUNCT_1:11;
then A5: f0 is_continuous_in x0 by NFCONT_3:def 2;
the carrier of (REAL-NS n) = dom G by FUNCT_2:def 1;
then G | (dom G) is_continuous_in f0 /. x0 by A1, NFCONT_1:def 7;
hence G * f0 is_continuous_in x0 by A4, A5, NFCONT_3:15; :: thesis: verum

end;

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 H₁( 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 = H₁(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 :: 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 . t by A11, A9, A7, FUNCT_1:47
.= integral (Gf,a,t) by A8, A12 ; :: thesis: 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 ;

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
thus ((REAL --> y0) | ['a,b']) . t = (REAL --> y0) . t by A16, A14, A7, FUNCT_1:47
.= y0 by XREAL_0:def 1, FUNCOP_1:7 ; :: thesis: verum

end;

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 ; :: thesis: S₁[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 A19: t in ['a,b'] ; :: thesis: 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 ; :: thesis: verum

end;

hence S₁[x,y] by A18, A3; :: thesis: 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 S₁[x,F . x] from FUNCT_2:sch 3(A2);
take F ; :: thesis: 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; :: thesis: verum