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;