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

hence
NumberOnLevel (n,T) is one-to-one
by FUNCT_1:def 4; :: thesis: verumx1 = 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;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