let T be full Tree; :: thesis: for n being non empty Element of NAT holds (FinSeqLevel n,T) . 1 = 0* n
A1: T = {0 ,1} * by Def2;
let n be non empty Element of NAT ; :: thesis: (FinSeqLevel n,T) . 1 = 0* n
0* n in T -level n by A1, Th10;
then A2: 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 A2, FUNCT_1:54; :: thesis: verum