set S = divs A;
let g1, g2 be PartFunc of divs A, REAL ; :: thesis: ( dom g1 = divs A & ( for D being Element of divs A st D in dom g1 holds
g1 . D = lower_sum f,D ) & dom g2 = divs A & ( for D being Element of divs A st D in dom g2 holds
g2 . D = lower_sum f,D ) implies g1 = g2 )
assume that
A7: ( dom g1 = divs A & ( for D being Element of divs A st D in dom g1 holds
g1 . D = lower_sum f,D ) ) and
A8: ( dom g2 = divs A & ( for D being Element of divs A st D in dom g2 holds
g2 . D = lower_sum f,D ) ) ; :: thesis: g1 = g2

now

let D be Element of divs A; :: thesis: ( D in dom g1 implies g1 . D = g2 . D )
assume D in dom g1 ; :: thesis: g1 . D = g2 . D
g1 . D = lower_sum f,D by A7;
hence g1 . D = g2 . D by A8; :: thesis: verum

end;

hence g1 = g2 by A7, A8, PARTFUN1:34; :: thesis: verum