now :: thesis: for x1, x2 being object st x1 in dom (NumberOnLevel (n,T)) & x2 in dom (NumberOnLevel (n,T)) & (NumberOnLevel (n,T)) . x1 = (NumberOnLevel (n,T)) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (NumberOnLevel (n,T)) & x2 in dom (NumberOnLevel (n,T)) & (NumberOnLevel (n,T)) . x1 = (NumberOnLevel (n,T)) . x2 implies x1 = x2 )
assume that
A1: x1 in dom (NumberOnLevel (n,T)) and
A2: x2 in dom (NumberOnLevel (n,T)) and
A3: (NumberOnLevel (n,T)) . x1 = (NumberOnLevel (n,T)) . x2 ; :: thesis: x1 = x2
A4: x1 in T -level n by A1, FUNCT_2:def 1;
then x1 in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider t1 being Element of T such that
A5: t1 = x1 and
A6: len t1 = n ;
A7: x2 in T -level n by A2, FUNCT_2:def 1;
then x2 in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider t2 being Element of T such that
A8: t2 = x2 and
A9: len t2 = n ;
len (Rev t2) = n by A9, FINSEQ_5:def 3;
then reconsider F2 = Rev t2 as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;
len (Rev t1) = n by A6, FINSEQ_5:def 3;
then reconsider F1 = Rev t1 as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;
(Absval F1) + 1 = (NumberOnLevel (n,T)) . x1 by A4, A5, Def1
.= (Absval F2) + 1 by A3, A7, A8, Def1 ;
hence x1 = x2 by A5, A8, BINARI_3:2, BINARI_3:3; :: thesis: verum

end;

hence NumberOnLevel (n,T) is one-to-one by FUNCT_1:def 4; :: thesis: verum