theorem :: TREES_3:66

for T1, T2 being Tree holds (^ T1) with-replacement (<*0*>,T2) = ^ T2