let F1, F2 be Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)); :: 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 & F1 . 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)) ) ) ) & ( 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 & F2 . 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)) ) ) ) implies F1 = F2 )

assume A24: 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 & F1 . 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)) ) ) ; :: thesis: ( ex x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) st

for f, g, Gf being continuous PartFunc of REAL, the carrier of X holds

( not x = f or not F2 . x = g or not dom f = ['a,b'] or not dom g = ['a,b'] or not Gf = G * f or ex t being Real st

( t in ['a,b'] & not g /. t = y0 + (integral (Gf,a,t)) ) ) or F1 = F2 )

assume A25: 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 & F2 . 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)) ) ) ; :: thesis: F1 = F2

( x = f & F1 . 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)) ) ) ) & ( 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 & F2 . 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)) ) ) ) implies F1 = F2 )

assume A24: 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 & F1 . 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)) ) ) ; :: thesis: ( ex x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) st

for f, g, Gf being continuous PartFunc of REAL, the carrier of X holds

( not x = f or not F2 . x = g or not dom f = ['a,b'] or not dom g = ['a,b'] or not Gf = G * f or ex t being Real st

( t in ['a,b'] & not g /. t = y0 + (integral (Gf,a,t)) ) ) or F1 = F2 )

assume A25: 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 & F2 . 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)) ) ) ; :: thesis: F1 = F2

now :: thesis: for x being Element of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds F1 . x = F2 . x

hence
F1 = F2
by FUNCT_2:def 8; :: thesis: verumlet x be Element of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)); :: thesis: F1 . x = F2 . x

consider f1, g1, Gf1 being continuous PartFunc of REAL, the carrier of X such that

A26: ( x = f1 & F1 . x = g1 & dom f1 = ['a,b'] & dom g1 = ['a,b'] & Gf1 = G * f1 & ( for t being Real st t in ['a,b'] holds

g1 /. t = y0 + (integral (Gf1,a,t)) ) ) by A24;

consider f2, g2, Gf2 being continuous PartFunc of REAL, the carrier of X such that

A27: ( x = f2 & F2 . x = g2 & dom f2 = ['a,b'] & dom g2 = ['a,b'] & Gf2 = G * f2 & ( for t being Real st t in ['a,b'] holds

g2 /. t = y0 + (integral (Gf2,a,t)) ) ) by A25;

end;consider f1, g1, Gf1 being continuous PartFunc of REAL, the carrier of X such that

A26: ( x = f1 & F1 . x = g1 & dom f1 = ['a,b'] & dom g1 = ['a,b'] & Gf1 = G * f1 & ( for t being Real st t in ['a,b'] holds

g1 /. t = y0 + (integral (Gf1,a,t)) ) ) by A24;

consider f2, g2, Gf2 being continuous PartFunc of REAL, the carrier of X such that

A27: ( x = f2 & F2 . x = g2 & dom f2 = ['a,b'] & dom g2 = ['a,b'] & Gf2 = G * f2 & ( for t being Real st t in ['a,b'] holds

g2 /. t = y0 + (integral (Gf2,a,t)) ) ) by A25;

now :: thesis: for t being object st t in dom g1 holds

g1 . t = g2 . t

hence
F1 . x = F2 . x
by A26, A27, FUNCT_1:2; :: thesis: verumg1 . t = g2 . t

let t be object ; :: thesis: ( t in dom g1 implies g1 . t = g2 . t )

assume A28: t in dom g1 ; :: thesis: g1 . t = g2 . t

then reconsider t0 = t as Real ;

A29: g1 /. t = y0 + (integral (Gf2,a,t0)) by A27, A28, A26

.= g2 /. t by A28, A27, A26 ;

thus g1 . t = g1 /. t by A28, PARTFUN1:def 6

.= g2 . t by A26, A27, A28, A29, PARTFUN1:def 6 ; :: thesis: verum

end;assume A28: t in dom g1 ; :: thesis: g1 . t = g2 . t

then reconsider t0 = t as Real ;

A29: g1 /. t = y0 + (integral (Gf2,a,t0)) by A27, A28, A26

.= g2 /. t by A28, A27, A26 ;

thus g1 . t = g1 /. t by A28, PARTFUN1:def 6

.= g2 . t by A26, A27, A28, A29, PARTFUN1:def 6 ; :: thesis: verum