let T be full Tree; for n being non zero Nat holds (FinSeqLevel (n,T)) . 1 = 0* n
let n be non zero Nat; (FinSeqLevel (n,T)) . 1 = 0* n
T = {0,1} *
by Def2;
then
0* n in T -level n
by Th10;
then A1:
0* n in dom (NumberOnLevel (n,T))
by FUNCT_2:def 1;
1 = (NumberOnLevel (n,T)) . (0* n)
by Th13;
hence
(FinSeqLevel (n,T)) . 1 = 0* n
by A1, FUNCT_1:32; verum