theorem Th88: :: COMPUT_1:89

for i being Nat holds
( [pred] . <*0*> = 0 & [pred] . <*(i + 1)*> = i )