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