let T be full Tree; :: thesis: for n being non zero Nat
for y being Element of n -tuples_on BOOLEAN st y = 0* n holds
(NumberOnLevel (n,T)) . ('not' y) = 2 to_power n
let n be non zero Nat; :: thesis: for y being Element of n -tuples_on BOOLEAN st y = 0* n holds
(NumberOnLevel (n,T)) . ('not' y) = 2 to_power n
let y be Element of n -tuples_on BOOLEAN; :: thesis: ( y = 0* n implies (NumberOnLevel (n,T)) . ('not' y) = 2 to_power n )
assume A1: y = 0* n ; :: thesis: (NumberOnLevel (n,T)) . ('not' y) = 2 to_power n
then A2: Rev ('not' y) = 'not' y by BINARI_3:9;
len (Rev ('not' y)) = len ('not' y) by FINSEQ_5:def 3
.= n by CARD_1:def 7 ;
then reconsider F = Rev ('not' y) as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;
reconsider ny = 'not' y as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;
T = {0,1} * by Def2;
then ny in T -level n by Th11;
hence (NumberOnLevel (n,T)) . ('not' y) = (Absval F) + 1 by Def1
.= ((2 to_power n) - 1) + 1 by A1, A2, BINARI_3:7
.= 2 to_power n ;
:: thesis: verum