theorem Lm3: :: DIOPHAN1:29

for i being Nat
for t being 1 _greater Nat holds (Partial_Union (Equal_Div_interval t)) . i = [.0,((i + 1) * (t ")).[