let F1, F2 be Division of A; :: thesis: ( F1 divide_into_equal n & F2 divide_into_equal n implies F1 = F2 )
assume that
A2: F1 divide_into_equal n and
A3: F2 divide_into_equal n ; :: thesis: F1 = F2
A4: ( len F1 = n & len F2 = n ) by A2, A3, INTEGRA4:def 1;
then A5: dom F1 = dom F2 by FINSEQ_3:29;
for n being Element of NAT st n in dom F1 holds
F1 . n = F2 . n

proof

let n be Element of NAT ; :: thesis: ( n in dom F1 implies F1 . n = F2 . n )
assume A6: n in dom F1 ; :: thesis: F1 . n = F2 . n
then F1 . n = (lower_bound A) + (((vol A) / (len F1)) * n) by A2, INTEGRA4:def 1;
hence F1 . n = F2 . n by A3, A6, A5, A4, INTEGRA4:def 1; :: thesis: verum

end;

hence F1 = F2 by A5, PARTFUN1:5; :: thesis: verum