set S = divs A;
defpred S₁[ set ] means $1 in divs A;
deffunc H₁( Element of divs A) -> Real = lower_sum f,$1;
consider g being PartFunc of divs A, REAL such that
A5: for D being Element of divs A holds
( D in dom g iff S₁[D] ) and
A6: for D being Element of divs A st D in dom g holds
g . D = H₁(D) from SEQ_1:sch 3();
take g ; :: thesis: ( dom g = divs A & ( for D being Element of divs A st D in dom g holds
g . D = lower_sum f,D ) )
[#] (divs A) = divs A ;
hence dom g = divs A by A5, SUBSET_1:8; :: thesis: for D being Element of divs A st D in dom g holds
g . D = lower_sum f,D

now

let D be Element of divs A; :: thesis: ( D in divs A implies g . D = lower_sum f,D )
assume D in divs A ; :: thesis: g . D = lower_sum f,D
D in dom g by A5;
hence g . D = lower_sum f,D by A6; :: thesis: verum

end;

hence for D being Element of divs A st D in dom g holds
g . D = lower_sum f,D ; :: thesis: verum