for z being object holds
( z in rng Nat2BL iff z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>} )
proof
let z be object ; :: thesis: ( z in rng Nat2BL iff z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>} )
hereby :: thesis: ( z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>} implies z in rng Nat2BL )
assume z in rng Nat2BL ; :: thesis: z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>}
then consider x being object such that
A2: ( x in NAT & z = Nat2BL . x ) by FUNCT_2:11;
reconsider x = x as Element of NAT by A2;
A3: Nat2BL . x = (LenBSeq x) -BinarySequence x by Def2;
set y = (LenBSeq x) -BinarySequence x;
per cases ( x = 0 or x <> 0 ) ;
suppose C1: x = 0 ; :: thesis: z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>}
then LenBSeq x = 1 by Def1;
then Nat2BL . x = <*0*> by LM0020, C1, BINARI_3:25, A3;
then z in {<*0*>} by A2, TARSKI:def 1;
hence z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>} by XBOOLE_0:def 3; :: thesis: verum
end;
suppose x <> 0 ; :: thesis: z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>}
then consider n being Nat such that
P1: ( 2 to_power n <= x & x < 2 to_power (n + 1) & LenBSeq x = n + 1 ) by Def1;
P2: (LenBSeq x) -BinarySequence x in BOOLEAN * by A3, FUNCT_2:5;
per cases ( n <> 0 or n = 0 ) ;
suppose n <> 0 ; :: thesis: z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>}
then ((LenBSeq x) -BinarySequence x) . (LenBSeq x) = 1 by P1, BINARI_3:29;
then ((LenBSeq x) -BinarySequence x) . (len ((LenBSeq x) -BinarySequence x)) = 1 by CARD_1:def 7;
then z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } by P2, A2, A3;
hence z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>} by XBOOLE_0:def 3; :: thesis: verum
end;
suppose C1: n = 0 ; :: thesis: z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>}
then ( 1 <= x & x < 1 + 1 ) by POWER:24, POWER:25, P1;
then ( 1 <= x & x <= 1 ) by NAT_1:13;
then x = 1 by XXREAL_0:1;
then C2: x = 2 to_power n by C1, POWER:24;
(n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*1*> by BINARI_3:28
.= {} ^ <*1*> by C1
.= <*1*> by FINSEQ_1:34 ;
then ( len ((LenBSeq x) -BinarySequence x) = 1 & ((LenBSeq x) -BinarySequence x) . 1 = 1 ) by FINSEQ_1:40, P1, C2;
then z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } by P2, A2, A3;
hence z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>} by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
end;
end;
assume z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>} ; :: thesis: z in rng Nat2BL
then ( z in { x where x is Element of BOOLEAN * : x . (len x) = 1 } or z in {<*0*>} ) by XBOOLE_0:def 3;
per cases then ( ex x being Element of BOOLEAN * st
( z = x & x . (len x) = 1 ) or z = <*0*> ) by TARSKI:def 1;
suppose ex x being Element of BOOLEAN * st
( z = x & x . (len x) = 1 ) ; :: thesis: z in rng Nat2BL
then consider x being Element of BOOLEAN * such that
A3: ( z = x & x . (len x) = 1 ) ;
set n = len x;
x is Element of (len x) -tuples_on BOOLEAN by FINSEQ_2:92;
then reconsider x = x as Tuple of len x, BOOLEAN ;
set L = Absval x;
A4: Nat2BL . (Absval x) = (LenBSeq (Absval x)) -BinarySequence (Absval x) by Def2;
Absval x < 2 to_power (LenBSeq (Absval x)) by LM006;
then A5: Absval ((LenBSeq (Absval x)) -BinarySequence (Absval x)) = Absval x by BINARI_3:35;
len x <> 0 by A3;
then 0 < len x ;
then 0 + 1 <= len x by NAT_1:13;
then reconsider n1 = (len x) - 1 as Element of NAT by INT_1:5;
x . (n1 + 1) = 1 by A3;
then X3: ( 2 to_power n1 <= Absval x & Absval x < 2 to_power (n1 + 1) ) by LM0071;
then 0 < Absval x by POWER:34;
then LenBSeq (Absval x) = len x by Def1, X3;
then z = Nat2BL . (Absval x) by A4, A3, BINARI_3:2, A5;
hence z in rng Nat2BL by FUNCT_2:4; :: thesis: verum
end;
end;
end;
hence rng Nat2BL = { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>} by TARSKI:2; :: thesis: verum