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

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

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

now :: thesis: for t being object st t in dom g1 holds
g1 . 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;

hence F1 . x = F2 . x by A26, A27, FUNCT_1:2; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:def 8; :: thesis: verum