<*0*> = 0* 1 by FINSEQ_2:59;