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

let n be non zero Nat; :: thesis: (NumberOnLevel (n,T)) . (0* n) = 1

A1: len (Rev (0* n)) = len (0* n) by FINSEQ_5:def 3

.= n by CARD_1:def 7 ;

A2: T = {0,1} * by Def2;

then 0* n is Element of T by BINARI_3:4;

then Rev (0* n) is FinSequence of BOOLEAN by Lm3;

then reconsider F = Rev (0* n) as Element of n -tuples_on BOOLEAN by A1, FINSEQ_2:92;

0* n in T -level n by A2, Th10;

hence (NumberOnLevel (n,T)) . (0* n) = (Absval F) + 1 by Def1

.= 0 + 1 by BINARI_3:6, BINARI_3:8

.= 1 ;

:: thesis: verum

let n be non zero Nat; :: thesis: (NumberOnLevel (n,T)) . (0* n) = 1

A1: len (Rev (0* n)) = len (0* n) by FINSEQ_5:def 3

.= n by CARD_1:def 7 ;

A2: T = {0,1} * by Def2;

then 0* n is Element of T by BINARI_3:4;

then Rev (0* n) is FinSequence of BOOLEAN by Lm3;

then reconsider F = Rev (0* n) as Element of n -tuples_on BOOLEAN by A1, FINSEQ_2:92;

0* n in T -level n by A2, Th10;

hence (NumberOnLevel (n,T)) . (0* n) = (Absval F) + 1 by Def1

.= 0 + 1 by BINARI_3:6, BINARI_3:8

.= 1 ;

:: thesis: verum