theorem :: TREES_3:75

for T, T1, T2 being Tree holds
( (tree (T1,T2)) with-replacement (<*0*>,T) = tree (T,T2) & (tree (T1,T2)) with-replacement (<*1*>,T) = tree (T1,T) )