X1: 2 = 2 to_power 1 ;
LenBSeq 2 = [\(log (2,2))/] + 1 by EXL2
.= [\1/] + 1 by POWER:52
.= 1 + 1 by INT_1:25 ;
then Nat2BL . 2 = 2 -BinarySequence 2 by BINARI_6:def 2
.= <*0,1*> by BINARI_6:4, X1, BINARI_3:28 ;
hence Nat2BL . 2 = <*0,1*> ; :: thesis: verum