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 ();
X1: the carrier of X = dom G by FUNCT_2:def 1;
A2: for x being Element of the carrier of () ex y being Element of the carrier of () st S1[x,y]
proof
let x be Element of the carrier of (); :: thesis: ex y being Element of the carrier of () 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 ;
hence G * f0 is_continuous_in x0 by ; :: 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 ;
A7: ['a,b'] = [.a,b.] by ;
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 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
.= F0 . t by
.= integral (Gf,a,t) by ; :: 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
.= (REAL --> y0) . t by
.= y0 by ;
:: 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 ;
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 () by ;
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 ; :: thesis: verum
end;
hence S1[x,y] by A19, A3; :: thesis: verum
end;
consider F being Function of the carrier of (), the carrier of () such that
A23: for x being Element of the carrier of () holds S1[x,F . x] from take F ; :: thesis: for x being VECTOR of () 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 () 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