let T be full Tree; :: thesis: for n being non zero Nat holds (FinSeqLevel (n,T)) . 1 = 0* n

let n be non zero 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:32; :: thesis: verum

let n be non zero 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:32; :: thesis: verum