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
(FinSeqLevel n,T) . (2 to_power n) = 'not' y
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
(FinSeqLevel n,T) . (2 to_power n) = 'not' y
let y be Tuple of n,BOOLEAN ; :: thesis: ( y = 0* n implies (FinSeqLevel n,T) . (2 to_power n) = 'not' y )
assume A2: y = 0* n ; :: thesis: (FinSeqLevel n,T) . (2 to_power n) = 'not' y
'not' y in T -level n by A1, Th11;
then A3: 'not' y in dom (NumberOnLevel n,T) by FUNCT_2:def 1;
2 to_power n = (NumberOnLevel n,T) . ('not' y) by A2, Th14;
hence (FinSeqLevel n,T) . (2 to_power n) = 'not' y by A3, FUNCT_1:54; :: thesis: verum