let T be full Tree; :: thesis: for n being non empty Element of NAT holds (FinSeqLevel n,T) . 1 = 0* n
let n be non empty Element of NAT ; :: thesis: (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:54; :: thesis: verum