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
(FinSeqLevel (n,T)) . (2 to_power n) = 'not' y
let n be non zero 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:131;
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:32; :: thesis: verum