let t be DecoratedTree; :: thesis: t | (<*> NAT ) = t
A1: ( dom (t | (<*> NAT )) = (dom t) | (<*> NAT ) & (dom t) | (<*> NAT ) = dom t ) by TREES_1:60, TREES_2:def 11;

now

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 11
.= t . p by FINSEQ_1:47 ;
:: thesis: verum

end;

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