theorem :: TREES_1:31

for T being Tree holds T | (<*> NAT) = T