reconsider k = n as non zero Nat ;
T = {0,1} *
by Def2;
then A1:
not T -level n is empty
by Th10;
for y being object holds
( y in Seg (2 to_power n) iff ex x being object st
( x in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . x ) )
proof
let y be
object ;
( y in Seg (2 to_power n) iff ex x being object st
( x in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . x ) )
thus
(
y in Seg (2 to_power n) implies ex
x being
object st
(
x in dom (NumberOnLevel (k,T)) &
y = (NumberOnLevel (k,T)) . x ) )
( ex x being object st
( x in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . x ) implies y in Seg (2 to_power n) )proof
assume A2:
y in Seg (2 to_power n)
;
ex x being object st
( x in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . x )
take
((NumberOnLevel (n,T)) ") . y
;
( ((NumberOnLevel (n,T)) ") . y in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . (((NumberOnLevel (n,T)) ") . y) )
Seg (2 to_power n) c= rng (NumberOnLevel (n,T))
by Th12;
hence
(
((NumberOnLevel (n,T)) ") . y in dom (NumberOnLevel (k,T)) &
y = (NumberOnLevel (k,T)) . (((NumberOnLevel (n,T)) ") . y) )
by A2, FUNCT_1:32;
verum
end;
given x being
object 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:92;
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:1;
verum
end;
then
rng (NumberOnLevel (n,T)) = Seg (2 to_power n)
by FUNCT_1:def 3;
then A9:
dom ((NumberOnLevel (k,T)) ") = Seg (2 to_power n)
by FUNCT_1:33;
rng ((NumberOnLevel (k,T)) ") =
dom (NumberOnLevel (k,T))
by FUNCT_1:33
.=
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:2;
hence
(NumberOnLevel (n,T)) " is FinSequence of T -level n
by A1, FINSEQ_2:25; verum