let g1, g2 be PartFunc of (divs A),REAL; :: thesis:
assume that
A9: dom g1 = divs A and
A10: for D being Division of A st D in dom g1 holds
g1 . D = lower_sum (f,D) and
A11: dom g2 = divs A and
A12: for D being Division of A st D in dom g2 holds
g2 . D = lower_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 = lower_sum (f,D1) by A9, A10;
hence g1 . D = g2 . D by A11, A12; :: thesis:

end;