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:22;
then (T | p) . (<*> NAT) = T . (p ^ (<*> NAT)) by TREES_2:def 10
.= T . p by FINSEQ_1:34 ;
hence T . p = (T | p) . {} ; :: thesis: verum