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