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