now 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 = x2let x1,
x2 be
object ;
( 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
;
x1 = x2A4:
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;
verum end;
hence
NumberOnLevel (n,T) is one-to-one
by FUNCT_1:def 4; verum