let n be Element of NAT ; :: thesis: for a, b being Real

for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) )

let a, b be Real; :: thesis: for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) )

deffunc H_{1}( Real) -> Element of the carrier of (REAL-NS n) = 0. (REAL-NS n);

let f be PartFunc of REAL,(REAL-NS n); :: thesis: ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) )

defpred S_{1}[ set ] means $1 in ].a,b.[;

deffunc H_{2}( Real) -> Element of the carrier of (REAL-NS n) = integral (f,a,$1);

consider F being Function such that

A1: ( dom F = REAL & ( for x being Element of REAL holds

( ( S_{1}[x] implies F . x = H_{2}(x) ) & ( not S_{1}[x] implies F . x = H_{1}(x) ) ) ) )
from PARTFUN1:sch 4();

then reconsider F = F as PartFunc of REAL,(REAL-NS n) by A1, RELSET_1:4;

take F ; :: thesis: ( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) )

thus ( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) ) by A1; :: thesis: verum

for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) )

let a, b be Real; :: thesis: for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) )

deffunc H

let f be PartFunc of REAL,(REAL-NS n); :: thesis: ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) )

defpred S

deffunc H

consider F being Function such that

A1: ( dom F = REAL & ( for x being Element of REAL holds

( ( S

now :: thesis: for y being object st y in rng F holds

y in the carrier of (REAL-NS n)

then
rng F c= the carrier of (REAL-NS n)
;y in the carrier of (REAL-NS n)

let y be object ; :: thesis: ( y in rng F implies y in the carrier of (REAL-NS n) )

assume y in rng F ; :: thesis: y in the carrier of (REAL-NS n)

then consider x being object such that

A2: x in dom F and

A3: y = F . x by FUNCT_1:def 3;

reconsider x = x as Element of REAL by A1, A2;

end;assume y in rng F ; :: thesis: y in the carrier of (REAL-NS n)

then consider x being object such that

A2: x in dom F and

A3: y = F . x by FUNCT_1:def 3;

reconsider x = x as Element of REAL by A1, A2;

A4: now :: thesis: ( not x in ].a,b.[ implies y in the carrier of (REAL-NS n) )

assume
not x in ].a,b.[
; :: thesis: y in the carrier of (REAL-NS n)

then F . x = 0. (REAL-NS n) by A1;

hence y in the carrier of (REAL-NS n) by A3; :: thesis: verum

end;then F . x = 0. (REAL-NS n) by A1;

hence y in the carrier of (REAL-NS n) by A3; :: thesis: verum

now :: thesis: ( x in ].a,b.[ implies y in the carrier of (REAL-NS n) )

hence
y in the carrier of (REAL-NS n)
by A4; :: thesis: verumassume
x in ].a,b.[
; :: thesis: y in the carrier of (REAL-NS n)

then F . x = integral (f,a,x) by A1;

hence y in the carrier of (REAL-NS n) by A3; :: thesis: verum

end;then F . x = integral (f,a,x) by A1;

hence y in the carrier of (REAL-NS n) by A3; :: thesis: verum

then reconsider F = F as PartFunc of REAL,(REAL-NS n) by A1, RELSET_1:4;

take F ; :: thesis: ( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) )

thus ( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) ) by A1; :: thesis: verum