let T be full Tree; :: thesis: (FinSeqLevel (1,T)) . 1 = <*0*>
thus (FinSeqLevel (1,T)) . 1 = 0* 1 by Th15
.= <*0*> by FINSEQ_2:59 ; :: thesis: verum