let n be Nat; 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*>
; verum