let T, T1 be finite DecoratedTree; :: thesis: for p being Element of dom T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
let p be Element of dom T; :: thesis: (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
A1: ( card (dom T) = card T & card (dom T1) = card T1 ) by CARD_1:62;
A2: ( card (dom (T with-replacement (p,T1))) = card (T with-replacement (p,T1)) & card (dom (T | p)) = card (T | p) ) by CARD_1:62;
( dom (T with-replacement (p,T1)) = (dom T) with-replacement (p,(dom T1)) & dom (T | p) = (dom T) | p ) by TREES_2:def 10, TREES_2:def 11;
hence (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1) by A1, A2, Th16; :: thesis: verum