let g1, g2 be PartFunc of (divs A),REAL; :: thesis:
assume that
A3: dom g1 = divs A and
A4: for D being Division of A st D in dom g1 holds
g1 . D = upper_sum (f,D) and
A5: dom g2 = divs A and
A6: for D being Division of A st D in dom g2 holds
g2 . D = upper_sum (f,D) ; :: thesis:

let D be Element of divs A; :: thesis:
reconsider D1 = D as Division of A by Def3;
assume D in dom g1 ; :: thesis:
g1 . D = upper_sum (f,D1) by A3, A4;
hence g1 . D = g2 . D by A5, A6; :: thesis:

end;