defpred S1[ Element of divs A, set ] means ex D being Division of A st
( D = $1 & $2 = lower_sum (f,D) );
A5:
for x being Element of divs A ex y being Element of REAL st S1[x,y]
proof
let x be
Element of
divs A;
ex y being Element of REAL st S1[x,y]
reconsider x =
x as
Division of
A by Def2;
take
lower_sum (
f,
x)
;
( lower_sum (f,x) is set & lower_sum (f,x) is Element of REAL & S1[x, lower_sum (f,x)] )
thus
(
lower_sum (
f,
x) is
set &
lower_sum (
f,
x) is
Element of
REAL &
S1[
x,
lower_sum (
f,
x)] )
;
verum
end;
consider g being Function of (divs A),REAL such that
A6:
for x being Element of divs A holds S1[x,g . x]
from FUNCT_2:sch 3(A5);
take
g
; for D being Division of A holds g . D = lower_sum (f,D)
let D be Division of A; g . D = lower_sum (f,D)
reconsider D1 = D as Element of divs A by Def2;
S1[D1,g . D1]
by A6;
hence
g . D = lower_sum (f,D)
; verum