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 }
proof
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;
0 in NAT ;
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