let T be full Tree; :: thesis: for n being non empty Element of NAT
for y being Tuple of n,BOOLEAN st y = 0* n holds
(NumberOnLevel n,T) . ('not' y) = 2 to_power n
A1: T = {0 ,1} * by Def2;
let n be non empty Element of NAT ; :: thesis: for y being Tuple of n,BOOLEAN st y = 0* n holds
(NumberOnLevel n,T) . ('not' y) = 2 to_power n
let y be Tuple of n,BOOLEAN ; :: thesis: ( y = 0* n implies (NumberOnLevel n,T) . ('not' y) = 2 to_power n )
assume A2: y = 0* n ; :: thesis: (NumberOnLevel n,T) . ('not' y) = 2 to_power n
A3: 'not' y in T -level n by A1, Th11;
len (Rev ('not' y)) = len ('not' y) by FINSEQ_5:def 3
.= n by FINSEQ_1:def 18 ;
then reconsider F = Rev ('not' y) as Tuple of n,BOOLEAN by FINSEQ_2:110;
A4: Rev ('not' y) = 'not' y by A2, BINARI_3:10;
thus (NumberOnLevel n,T) . ('not' y) = (Absval F) + 1 by A3, Def1
.= ((2 to_power n) - 1) + 1 by A2, A4, BINARI_3:8
.= 2 to_power n ; :: thesis: verum