deffunc H_{1}( Real) -> Element of NAT = 0 ;

let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL ex F being PartFunc of REAL,REAL st

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

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

let f be PartFunc of REAL,REAL; :: thesis: ex F being PartFunc of REAL,REAL 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) -> object = 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 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

let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL ex F being PartFunc of REAL,REAL st

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

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

let f be PartFunc of REAL,REAL; :: thesis: ex F being PartFunc of REAL,REAL 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 REAL

then
rng F c= REAL
;y in REAL

let y be object ; :: thesis: ( y in rng F implies y in REAL )

assume y in rng F ; :: thesis: y in REAL

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 REAL

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 REAL )

assume
not x in ].a,b.[
; :: thesis: y in REAL

then F . x = In (0,REAL) by A1;

hence y in REAL by A3; :: thesis: verum

end;then F . x = In (0,REAL) by A1;

hence y in REAL by A3; :: thesis: verum

now :: thesis: ( x in ].a,b.[ implies y in REAL )

hence
y in REAL
by A4; :: thesis: verumassume
x in ].a,b.[
; :: thesis: y in REAL

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

hence y in REAL by A3, XREAL_0:def 1; :: thesis: verum

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

hence y in REAL by A3, XREAL_0:def 1; :: thesis: verum

then reconsider F = F as PartFunc of REAL,REAL 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