let T be full Tree; :: thesis: for n being non empty Element of NAT
for y being Element of n -tuples_on BOOLEAN st y = 0* n holds
(FinSeqLevel n,T) . (2 to_power n) = 'not' y
let n be non empty Element of NAT ; :: thesis: for y being Element of n -tuples_on BOOLEAN st y = 0* n holds
(FinSeqLevel n,T) . (2 to_power n) = 'not' y
let y be Element of n -tuples_on BOOLEAN ; :: thesis: ( y = 0* n implies (FinSeqLevel n,T) . (2 to_power n) = 'not' y )
reconsider ny = 'not' y as Element of n -tuples_on BOOLEAN by FINSEQ_2:151;
T = {0 ,1} * by Def2;
then ny in T -level n by Th11;
then A1: 'not' y in dom (NumberOnLevel n,T) by FUNCT_2:def 1;
assume y = 0* n ; :: thesis: (FinSeqLevel n,T) . (2 to_power n) = 'not' y
then 2 to_power n = (NumberOnLevel n,T) . ('not' y) by Th14;
hence (FinSeqLevel n,T) . (2 to_power n) = 'not' y by A1, FUNCT_1:54; :: thesis: verum