theorem :: BINTREE2:22

for T being full Tree holds (FinSeqLevel (1,T)) . 1 = <*0*>