for i being natural Number holds i -' 2 = (i -' 1) -' 1