defpred S1[ Element of divs A, set ] means ex D being Division of A st
( D = $1 & $2 = upper_sum (f,D) );
A1:
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
upper_sum (
f,
x)
;
( upper_sum (f,x) is set & upper_sum (f,x) is Element of REAL & S1[x, upper_sum (f,x)] )
thus
(
upper_sum (
f,
x) is
set &
upper_sum (
f,
x) is
Element of
REAL &
S1[
x,
upper_sum (
f,
x)] )
;
verum
end;
consider g being Function of (divs A),REAL such that
A2:
for x being Element of divs A holds S1[x,g . x]
from FUNCT_2:sch 3(A1);
take
g
; for D being Division of A holds g . D = upper_sum (f,D)
let D be Division of A; g . D = upper_sum (f,D)
reconsider D1 = D as Element of divs A by Def2;
S1[D1,g . D1]
by A2;
hence
g . D = upper_sum (f,D)
; verum