now let x1,
x2 be
set ;
:: 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 = 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
;
len (Rev t1) = n
by A6, FINSEQ_5:def 3;
then reconsider F1 =
Rev t1 as
Tuple of
n,
BOOLEAN by FINSEQ_2:110;
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
Tuple of
n,
BOOLEAN by FINSEQ_2:110;
(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 8; :: thesis: verum