let n be Element of NAT ; :: thesis: for a, b being Real
for f being PartFunc of REAL,() ex F being PartFunc of REAL,() 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,() ex F being PartFunc of REAL,() st
( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )

deffunc H1( Real) -> Element of the carrier of () = 0. ();
let f be PartFunc of REAL,(); :: thesis: ex F being PartFunc of 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) -> Element of the carrier of () = 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
now :: thesis: for y being object st y in rng F holds
y in the carrier of ()
let y be object ; :: thesis: ( y in rng F implies y in the carrier of () )
assume y in rng F ; :: thesis: y in the carrier of ()
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 () )
assume not x in ].a,b.[ ; :: thesis: y in the carrier of ()
then F . x = 0. () by A1;
hence y in the carrier of () by A3; :: thesis: verum
end;
now :: thesis: ( x in ].a,b.[ implies y in the carrier of () )
assume x in ].a,b.[ ; :: thesis: y in the carrier of ()
then F . x = integral (f,a,x) by A1;
hence y in the carrier of () by A3; :: thesis: verum
end;
hence y in the carrier of () by A4; :: thesis: verum
end;
then rng F c= the carrier of () ;
then reconsider F = F as PartFunc of REAL,() by ;
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