theorem Lm2: :: DIOPHAN1:28

for k being Nat
for t being 1 _greater Nat holds [.0,((k + 1) * (t ")).[ \/ [.((k + 1) * (t ")),((k + 2) * (t ")).[ = [.0,((k + 2) * (t ")).[