theorem Th16: :: PRE_CIRC:17

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