let t be DecoratedTree; :: thesis: t | (<*> NAT) = t
A1: dom (t | (<*> NAT)) = (dom t) | (<*> NAT) by TREES_2:def 10;

now :: thesis: for p being FinSequence of NAT st p in dom (t | (<*> NAT)) holds
(t | (<*> NAT)) . p = t . p

let p be FinSequence of NAT ; :: thesis: ( p in dom (t | (<*> NAT)) implies (t | (<*> NAT)) . p = t . p )
assume p in dom (t | (<*> NAT)) ; :: thesis: (t | (<*> NAT)) . p = t . p
hence (t | (<*> NAT)) . p = t . ({} ^ p) by A1, TREES_2:def 10
.= t . p by FINSEQ_1:34 ;
:: thesis: verum

end;

hence t | (<*> NAT) = t by A1, TREES_1:31; :: thesis: verum