theorem :: BINTREE2:23

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