deffunc H1( Real) -> Element of NAT = 0 ;
let a, b be Real; 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; 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 S1[ set ] means $1 in ].a,b.[;
deffunc H2( Real) -> object = integral (f,a,$1);
consider F being Function such that
A1:
( dom F = REAL & ( for x being Element of REAL holds
( ( S1[x] implies F . x = H2(x) ) & ( not S1[x] implies F . x = H1(x) ) ) ) )
from PARTFUN1:sch 4();
then
rng F c= REAL
;
then reconsider F = F as PartFunc of REAL,REAL by A1, RELSET_1:4;
take
F
; ( ].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; verum