let I be non empty closed_interval Subset of REAL; :: thesis: for D being Division of I holds
( divset (D,1) = [.(lower_bound I),(D . 1).] & ( for j being Nat st j in dom D & j <> 1 holds
divset (D,j) = [.(D . (j - 1)),(D . j).] ) )
let D be Division of I; :: thesis: ( divset (D,1) = [.(lower_bound I),(D . 1).] & ( for j being Nat st j in dom D & j <> 1 holds
divset (D,j) = [.(D . (j - 1)),(D . j).] ) )
rng D <> {} ;
then 1 in dom D by FINSEQ_3:32;
then ( lower_bound (divset (D,1)) = lower_bound I & upper_bound (divset (D,1)) = D . 1 ) by INTEGRA1:def 4;
hence divset (D,1) = [.(lower_bound I),(D . 1).] by INTEGRA1:4; :: thesis: for j being Nat st j in dom D & j <> 1 holds
divset (D,j) = [.(D . (j - 1)),(D . j).]
thus for j being Nat st j in dom D & j <> 1 holds
divset (D,j) = [.(D . (j - 1)),(D . j).] :: thesis: verum
proof
let j be Nat; :: thesis: ( j in dom D & j <> 1 implies divset (D,j) = [.(D . (j - 1)),(D . j).] )
assume that
A1: j in dom D and
A2: j <> 1 ; :: thesis: divset (D,j) = [.(D . (j - 1)),(D . j).]
( lower_bound (divset (D,j)) = D . (j - 1) & upper_bound (divset (D,j)) = D . j ) by A1, A2, INTEGRA1:def 4;
hence divset (D,j) = [.(D . (j - 1)),(D . j).] by INTEGRA1:4; :: thesis: verum
end;