defpred S₁[ Element of divs A, set ] means ex D being Division of A st
( D = $1 & $2 = lower_sum (f,D) );
A1: for x being Element of divs A ex y being Element of REAL st S₁[x,y]

proof

let x be Element of divs A; :: thesis: ex y being Element of REAL st S₁[x,y]
reconsider x = x as Division of A by Def3;
take lower_sum (f,x) ; :: thesis: S₁[x, lower_sum (f,x)]
thus S₁[x, lower_sum (f,x)] ; :: thesis: verum

end;

consider g being Function of (divs A),REAL such that
A8: for x being Element of divs A holds S₁[x,g . x] from FUNCT_2:sch 3(A1);
take g ; :: thesis: for D being Division of A holds g . D = lower_sum (f,D)
let D be Division of A; :: thesis: g . D = lower_sum (f,D)
reconsider D1 = D as Element of divs A by Def3;
S₁[D1,g . D1] by A8;
hence g . D = lower_sum (f,D) ; :: thesis: verum