let F1, F2 be Function of (),(); :: thesis: ( ( for x being VECTOR of () 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 () 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 () 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 () 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 () 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 () holds F1 . x = F2 . x
let x be Element of (); :: 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
.= g2 /. t by ;
thus g1 . t = g1 /. t by
.= g2 . t by ; :: thesis: verum
end;
hence F1 . x = F2 . x by ; :: thesis: verum
end;
hence F1 = F2 by FUNCT_2:def 8; :: thesis: verum