let A1, A2 be closed-interval Subset of REAL ; :: thesis: ( ( i = 1 & lower_bound A1 = lower_bound A & upper_bound A1 = D . i & lower_bound A2 = lower_bound A & upper_bound A2 = D . i implies A1 = A2 ) & ( not i = 1 & lower_bound A1 = D . (i - 1) & upper_bound A1 = D . i & lower_bound A2 = D . (i - 1) & upper_bound A2 = D . i implies A1 = A2 ) )

hereby :: thesis: ( not i = 1 & lower_bound A1 = D . (i - 1) & upper_bound A1 = D . i & lower_bound A2 = D . (i - 1) & upper_bound A2 = D . i implies A1 = A2 )

assume that
i = 1 and
A12: ( lower_bound A1 = lower_bound A & upper_bound A1 = D . i ) and
A13: ( lower_bound A2 = lower_bound A & upper_bound A2 = D . i ) ; :: thesis: A1 = A2
consider b being Real such that
A14: b = D . i ;
A1 = [.(lower_bound A),b.] by A12, A14, Th5;
hence A1 = A2 by A13, A14, Th5; :: thesis: verum

end;

assume that
i <> 1 and
A15: ( lower_bound A1 = D . (i - 1) & upper_bound A1 = D . i ) and
A16: ( lower_bound A2 = D . (i - 1) & upper_bound A2 = D . i ) ; :: thesis: A1 = A2
consider a, b being Real such that
A17: a = D . (i - 1) and
A18: b = D . i ;
A1 = [.a,b.] by A15, A17, A18, Th5;
hence A1 = A2 by A16, A17, A18, Th5; :: thesis: verum