theorem MMS1: :: NTALGO_2:8

for n being Element of NAT st 0 < n holds
(Nat2BL . n) . (LenBSeq n) = 1