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 = upper_sum f,D ) & dom g2 = divs A & ( for D being Element of divs A st D in dom g2 holds
g2 . D = upper_sum f,D ) implies g1 = g2 )
assume that
A3: ( dom g1 = divs A & ( for D being Element of divs A st D in dom g1 holds
g1 . D = upper_sum f,D ) ) and
A4: ( dom g2 = divs A & ( for D being Element of divs A st D in dom g2 holds
g2 . D = upper_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 = upper_sum f,D by A3;
hence g1 . D = g2 . D by A4; :: thesis: verum

end;

hence g1 = g2 by A3, A4, PARTFUN1:34; :: thesis: verum