let T be full Tree; :: thesis: (FinSeqLevel 1,T) . 2 = <*1*>
A1: 0* 1 = <*FALSE *> by FINSEQ_2:73;
thus (FinSeqLevel 1,T) . 2 = (FinSeqLevel 1,T) . (2 to_power 1) by POWER:30
.= <*1*> by A1, Th16, BINARI_3:15 ; :: thesis: verum