let A1, A2 be non empty 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 )
consider b being Real such that
A14: b = D . i ;
assume that
i = 1 and
A15: lower_bound A1 = lower_bound A and
A16: upper_bound A1 = D . i and
A17: lower_bound A2 = lower_bound A and
A18: upper_bound A2 = D . i ; :: thesis: A1 = A2
A1 = [.(lower_bound A),b.] by A15, A16, A14, Th2;
hence A1 = A2 by A17, A18, A14, Th2; :: thesis: verum
end;
assume that
i <> 1 and
A19: lower_bound A1 = D . (i - 1) and
A20: upper_bound A1 = D . i and
A21: lower_bound A2 = D . (i - 1) and
A22: upper_bound A2 = D . i ; :: thesis: A1 = A2
consider a, b being Real such that
A23: a = D . (i - 1) and
A24: b = D . i ;
A1 = [.a,b.] by A19, A20, A23, A24, Th2;
hence A1 = A2 by A21, A22, A23, A24, Th2; :: thesis: verum