let T be full Tree; :: thesis: (FinSeqLevel 1,T) . 2 = <*1*>
A1: 0* 1 = <*FALSE *> by FINSEQ_2:73;
reconsider t = <*FALSE *> as Element of 1 -tuples_on BOOLEAN by FINSEQ_2:151;
thus (FinSeqLevel 1,T) . 2 = (FinSeqLevel 1,T) . (2 to_power 1) by POWER:30
.= 'not' t by A1, Th16
.= <*1*> by BINARI_3:15 ; :: thesis: verum