theorem :: TREES_3:65

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