let f be Function of NAT,(BOOLEAN *); :: thesis: ( ( for x being Element of NAT holds f . x = (LenBSeq x) -BinarySequence x ) implies f is one-to-one )
assume AS1: for x being Element of NAT holds f . x = (LenBSeq x) -BinarySequence x ; :: thesis: f is one-to-one
for x1, x2 being object st x1 in NAT & x2 in NAT & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in NAT & x2 in NAT & f . x1 = f . x2 implies x1 = x2 )
assume A0: ( x1 in NAT & x2 in NAT & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider k1 = x1, k2 = x2 as Element of NAT ;
A3: (LenBSeq k1) -BinarySequence k1 = f . k1 by AS1
.= (LenBSeq k2) -BinarySequence k2 by AS1, A0 ;
NN: ( LenBSeq k1 is Element of NAT & LenBSeq k2 is Element of NAT ) by ORDINAL1:def 12;
(LenBSeq k1) -BinarySequence k1 in (LenBSeq k1) -tuples_on BOOLEAN by FINSEQ_2:131;
then A4: len ((LenBSeq k1) -BinarySequence k1) = LenBSeq k1 by NN, FINSEQ_2:132;
(LenBSeq k2) -BinarySequence k2 in (LenBSeq k2) -tuples_on BOOLEAN by FINSEQ_2:131;
then A5: LenBSeq k1 = LenBSeq k2 by A4, A3, NN, FINSEQ_2:132;
thus x1 = Absval ((LenBSeq k1) -BinarySequence k1) by LM007
.= x2 by LM007, A3, A5 ; :: thesis: verum
end;
hence f is one-to-one by FUNCT_2:19; :: thesis: verum