theorem :: PRE_CIRC:18

for T, T1 being finite DecoratedTree
for p being Element of dom T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)