let n be Element of NAT ; :: thesis: ( 0 < n implies (Nat2BL . n) . (LenBSeq n) = 1 )

assume AS: 0 < n ; :: thesis: (Nat2BL . n) . (LenBSeq n) = 1

assume AC: (Nat2BL . n) . (LenBSeq n) <> 1 ; :: thesis: contradiction

L1: Nat2BL . n = (LenBSeq n) -BinarySequence n by BINARI_6:def 2;

reconsider x = Nat2BL . n as Element of BOOLEAN * ;

LAC: not x in { y where y is Element of BOOLEAN * : y . (len y) = 1 }

then PO: 0 in dom Nat2BL by FUNCT_2:def 1;

n in NAT ;

then TLL: n in dom Nat2BL by FUNCT_2:def 1;

then x in rng Nat2BL by FUNCT_1:3;

then ( x in { y where y is Element of BOOLEAN * : y . (len y) = 1 } or x in {<*0*>} ) by BINARI_6:11, XBOOLE_0:def 3;

then Nat2BL . n = <*0*> by TARSKI:def 1, LAC;

hence contradiction by AS, TLL, PO, zerobs, BINARI_6:12; :: thesis: verum

assume AS: 0 < n ; :: thesis: (Nat2BL . n) . (LenBSeq n) = 1

assume AC: (Nat2BL . n) . (LenBSeq n) <> 1 ; :: thesis: contradiction

L1: Nat2BL . n = (LenBSeq n) -BinarySequence n by BINARI_6:def 2;

reconsider x = Nat2BL . n as Element of BOOLEAN * ;

LAC: not x in { y where y is Element of BOOLEAN * : y . (len y) = 1 }

proof

0 in NAT
;
assume
x in { y where y is Element of BOOLEAN * : y . (len y) = 1 }
; :: thesis: contradiction

then ex y being Element of BOOLEAN * st

( x = y & y . (len y) = 1 ) ;

hence contradiction by AC, L1, FINSEQ_3:153; :: thesis: verum

end;then ex y being Element of BOOLEAN * st

( x = y & y . (len y) = 1 ) ;

hence contradiction by AC, L1, FINSEQ_3:153; :: thesis: verum

then PO: 0 in dom Nat2BL by FUNCT_2:def 1;

n in NAT ;

then TLL: n in dom Nat2BL by FUNCT_2:def 1;

then x in rng Nat2BL by FUNCT_1:3;

then ( x in { y where y is Element of BOOLEAN * : y . (len y) = 1 } or x in {<*0*>} ) by BINARI_6:11, XBOOLE_0:def 3;

then Nat2BL . n = <*0*> by TARSKI:def 1, LAC;

hence contradiction by AS, TLL, PO, zerobs, BINARI_6:12; :: thesis: verum