let T be DecoratedTree; :: thesis: for p being FinSequence of NAT holds T . p = (T | p) . {}
let p be FinSequence of NAT ; :: thesis: T . p = (T | p) . {}
<*> NAT in (dom T) | p by TREES_1:47;
then (T | p) . (<*> NAT ) = T . (p ^ (<*> NAT )) by TREES_2:def 11
.= T . p by FINSEQ_1:47 ;
hence T . p = (T | p) . {} ; :: thesis: verum