theorem Th45: :: NAT_D:45

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