let g1, g2 be Function of (divs A),REAL; :: thesis: ( ( for D being Division of A holds g1 . D = lower_sum (f,D) ) & ( for D being Division of A holds g2 . D = lower_sum (f,D) ) implies g1 = g2 )
assume that
A7: for D being Division of A holds g1 . D = lower_sum (f,D) and
A8: for D being Division of A holds g2 . D = lower_sum (f,D) ; :: thesis: g1 = g2
let a be Element of divs A; :: according to FUNCT_2:def 8 :: thesis: g1 . a = g2 . a
reconsider d = a as Division of A by Def2;
thus g1 . a = lower_sum (f,d) by A7
.= g2 . a by A8 ; :: thesis: verum