reconsider k = n as non empty Element of NAT by ORDINAL1:def 13;
T = {0 ,1} *
by Def2;
then A1:
not T -level n is empty
by Th10;
for y being set holds
( y in Seg (2 to_power n) iff ex x being set st
( x in dom (NumberOnLevel k,T) & y = (NumberOnLevel k,T) . x ) )
proof
let y be
set ;
( y in Seg (2 to_power n) iff ex x being set st
( x in dom (NumberOnLevel k,T) & y = (NumberOnLevel k,T) . x ) )
thus
(
y in Seg (2 to_power n) implies ex
x being
set st
(
x in dom (NumberOnLevel k,T) &
y = (NumberOnLevel k,T) . x ) )
( ex x being set st
( x in dom (NumberOnLevel k,T) & y = (NumberOnLevel k,T) . x ) implies y in Seg (2 to_power n) )
given x being
set such that A3:
x in dom (NumberOnLevel k,T)
and A4:
y = (NumberOnLevel k,T) . x
;
y in Seg (2 to_power n)
A5:
x in T -level n
by A3, FUNCT_2:def 1;
then
x in { t where t is Element of T : len t = n }
by TREES_2:def 6;
then consider t being
Element of
T such that A6:
t = x
and A7:
len t = n
;
len (Rev t) = n
by A7, FINSEQ_5:def 3;
then reconsider F =
Rev t as
Element of
n -tuples_on BOOLEAN by FINSEQ_2:110;
Absval F < 2
to_power n
by BINARI_3:1;
then A8:
( 1
<= (Absval F) + 1 &
(Absval F) + 1
<= 2
to_power n )
by NAT_1:11, NAT_1:13;
y = (Absval F) + 1
by A4, A5, A6, Def1;
hence
y in Seg (2 to_power n)
by A8, FINSEQ_1:3;
verum
end;
then
rng (NumberOnLevel n,T) = Seg (2 to_power n)
by FUNCT_1:def 5;
then A9:
dom ((NumberOnLevel k,T) " ) = Seg (2 to_power n)
by FUNCT_1:55;
rng ((NumberOnLevel k,T) " ) =
dom (NumberOnLevel k,T)
by FUNCT_1:55
.=
T -level n
by FUNCT_2:def 1
;
then
(NumberOnLevel n,T) " is Function of (Seg (2 to_power n)),(T -level n)
by A9, FUNCT_2:4;
hence
(NumberOnLevel n,T) " is FinSequence of T -level n
by A1, FINSEQ_2:28; verum