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