let F1, F2 be Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)); ( ( 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)) ) )
; ( 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)) ) )
; F1 = F2
now for x being Element of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds F1 . x = F2 . xlet x be
Element of
(R_NormSpace_of_ContinuousFunctions (['a,b'],X));
F1 . x = F2 . xconsider 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 for t being object st t in dom g1 holds
g1 . t = g2 . tlet t be
object ;
( t in dom g1 implies g1 . t = g2 . t )assume A28:
t in dom g1
;
g1 . t = g2 . tthen 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
;
verum end; hence
F1 . x = F2 . x
by A26, A27, FUNCT_1:2;
verum end;
hence
F1 = F2
by FUNCT_2:def 8; verum