X1: 1 = 2 to_power 0 by POWER:24;
Nat2BL . 1 = 1 -BinarySequence 1 by BINARI_6:def 2, EXL1
.= (0* 0) ^ <*1*> by X1, BINARI_3:28
.= <*1*> by FINSEQ_1:34 ;
hence Nat2BL . 1 = <*1*> ; :: thesis: verum