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 by INT_1:25 ;

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

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 by INT_1:25 ;

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