theorem EXL1: :: NTALGO_2:3

LenBSeq 1 = 1