defpred S_{1}[ 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 S_{1}[x,y]

A23: for x being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds S_{1}[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

( $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 S

proof

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
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 S_{1}[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;

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 H_{1}( 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 = H_{1}(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;

set G1 = (REAL --> y0) | ['a,b'];

dom (REAL --> y0) = REAL ;

then A14: dom ((REAL --> y0) | ['a,b']) = ['a,b'] by RELAT_1:62;

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: S_{1}[x,y]

_{1}[x,y]
by A19, A3; :: thesis: verum

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

then reconsider Gf = G * f0 as continuous PartFunc of REAL, the carrier of X by NFCONT_3:def 2;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;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

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 H

consider F0 being Function of REAL, the carrier of X such that

A8: for x being Element of REAL holds F0 . x = H

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)

set G0 = REAL --> y0;(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;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

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

set g = ((REAL --> y0) | ['a,b']) + (F0 | ['a,b']);((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;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

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

now :: thesis: for t being Real st t in ['a,b'] holds

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

hence
Sg /. 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;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

A23: for x being Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds S

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