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:104;
A2: ( card (dom (T with-replacement p,T1)) = card (T with-replacement p,T1) & card (dom (T | p)) = card (T | p) ) by CARD_1:104;
( dom (T with-replacement p,T1) = (dom T) with-replacement p,(dom T1) & dom (T | p) = (dom T) | p ) by TREES_2:def 11, TREES_2:def 12;
hence (card (T with-replacement p,T1)) + (card (T | p)) = (card T) + (card T1) by A1, A2, Th22; :: thesis: verum