T = {0 ,1} *
by Def2;
then A1:
not T -level n is empty
by Th10;
reconsider k = n as non empty Element of NAT by ORDINAL1:def 13;
A2: rng ((NumberOnLevel k,T) " ) =
dom (NumberOnLevel k,T)
by FUNCT_1:55
.=
T -level n
by FUNCT_2:def 1
;
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 ;
:: thesis: ( 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 ) )
:: thesis: ( 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 A4:
x in dom (NumberOnLevel k,T)
and A5:
y = (NumberOnLevel k,T) . x
;
:: thesis: y in Seg (2 to_power n)
A6:
x in T -level n
by A4, 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 A7:
t = x
and A8:
len t = n
;
len (Rev t) = n
by A8, FINSEQ_5:def 3;
then reconsider F =
Rev t as
Tuple of
n,
BOOLEAN by FINSEQ_2:110;
A9:
y = (Absval F) + 1
by A5, A6, A7, Def1;
A10:
1
<= (Absval F) + 1
by NAT_1:11;
Absval F < 2
to_power n
by BINARI_3:1;
then
(Absval F) + 1
<= 2
to_power n
by NAT_1:13;
hence
y in Seg (2 to_power n)
by A9, A10, FINSEQ_1:3;
:: thesis: verum
end;
then
rng (NumberOnLevel n,T) = Seg (2 to_power n)
by FUNCT_1:def 5;
then
dom ((NumberOnLevel k,T) " ) = Seg (2 to_power n)
by FUNCT_1:55;
then
(NumberOnLevel n,T) " is Function of (Seg (2 to_power n)),(T -level n)
by A2, FUNCT_2:4;
hence
(NumberOnLevel n,T) " is FinSequence of T -level n
by A1, FINSEQ_2:28; :: thesis: verum