deffunc H₁( real number ) -> Element of NAT = 0 ;
let a, b be real number ; :: 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 number 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 number st x in ].a,b.[ holds
F . x = integral f,a,x ) )
defpred S₁[ set ] means $1 in ].a,b.[;
deffunc H₂( real number ) -> Element of REAL = integral f,a,$1;
consider F being Function such that
A1: ( dom F = REAL & ( for x being Element of REAL holds
( ( S₁[x] implies F . x = H₂(x) ) & ( not S₁[x] implies F . x = H₁(x) ) ) ) ) from PARTFUN1:sch 4();

now

let y be set ; :: thesis: ( y in rng F implies y in REAL )
assume y in rng F ; :: thesis: y in REAL
then consider x being set such that
A2: x in dom F and
A3: y = F . x by FUNCT_1:def 5;
reconsider x = x as Element of REAL by A1, A2;

A4: now

assume not x in ].a,b.[ ; :: thesis: y in REAL
then F . x = 0 by A1;
hence y in REAL by A3; :: thesis: verum

end;

now

assume x in ].a,b.[ ; :: thesis: y in REAL
then F . x = integral f,a,x by A1;
hence y in REAL by A3; :: thesis: verum

end;

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

end;

then rng F c= REAL by TARSKI:def 3;
then reconsider F = F as PartFunc of REAL ,REAL by A1, RELSET_1:11;
take F ; :: thesis: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) )
thus ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) ) by A1; :: thesis: verum