let n be Nat; :: thesis: Nat2BL . (2 |^ n) = (0* n) ^ <*1*>
X1: 2 |^ n = 2 to_power n ;
X3: LenBSeq (2 |^ n) = [\(log (2,(2 |^ n)))/] + 1 by EXL2
.= [\n/] + 1 by X1, POWER:def 3
.= n + 1 ;
2 |^ n is Element of NAT by ORDINAL1:def 12;
then Nat2BL . (2 |^ n) = (n + 1) -BinarySequence (2 |^ n) by X3, BINARI_6:def 2
.= (0* n) ^ <*1*> by BINARI_3:28, X1 ;
hence Nat2BL . (2 |^ n) = (0* n) ^ <*1*> ; :: thesis: verum