theorem LM0020: :: BINARI_6:4

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