let T, T1 be finite Tree; :: thesis: for p being Element of T holds (card (T with-replacement p,T1)) + (card (T | p)) = (card T) + (card T1)
let p be Element of T; :: thesis: (card (T with-replacement p,T1)) + (card (T | p)) = (card T) + (card T1)
defpred S₁[ Element of T] means not p is_a_prefix_of $1;
defpred S₂[ Element of T] means p is_a_prefix_of $1;
set A = { t where t is Element of T : S₁[t] } ;
set B = { t where t is Element of T : S₂[t] } ;
set C = { (p ^ t1) where t1 is Element of T1 : verum } ;
A1: { t where t is Element of T : S₁[t] } is Subset of T from DOMAIN_1:sch 7();
A2: { t where t is Element of T : S₂[t] } is Subset of T from DOMAIN_1:sch 7();
then reconsider A = { t where t is Element of T : S₁[t] } , B = { t where t is Element of T : S₂[t] } as finite set by A1;
A3: T with-replacement p,T1 = A \/ { (p ^ t1) where t1 is Element of T1 : verum } by Th14;
A4: A misses { (p ^ t1) where t1 is Element of T1 : verum }

proof

assume not A misses { (p ^ t1) where t1 is Element of T1 : verum } ; :: thesis: contradiction
then consider x being set such that
A5: x in A /\ { (p ^ t1) where t1 is Element of T1 : verum } by XBOOLE_0:4;
x in A by A5, XBOOLE_0:def 4;
then consider t being Element of T such that
A6: ( x = t & not p is_a_prefix_of t ) ;
x in { (p ^ t1) where t1 is Element of T1 : verum } by A5, XBOOLE_0:def 4;
then ex t1 being Element of T1 st x = p ^ t1 ;
hence contradiction by A6, TREES_1:8; :: thesis: verum

end;

now

let x be set ; :: thesis: ( ( not x in T or x in A or x in B ) & ( ( x in A or x in B ) implies x in T ) )

hereby :: thesis: ( ( x in A or x in B ) implies x in T )

assume x in T ; :: thesis: ( x in A or x in B )
then reconsider t = x as Element of T ;
( p is_a_prefix_of t or not p is_a_prefix_of t ) ;
hence ( x in A or x in B ) ; :: thesis: verum

end;

assume ( x in A or x in B ) ; :: thesis: x in T
hence x in T by A1, A2; :: thesis: verum

end;

then A7: T = A \/ B by XBOOLE_0:def 3;
A8: A misses B

proof

assume not A misses B ; :: thesis: contradiction
then consider x being set such that
A9: x in A /\ B by XBOOLE_0:4;
( x in A & x in B ) by A9, XBOOLE_0:def 4;
then ( ex t being Element of T st
( x = t & not p is_a_prefix_of t ) & ex t being Element of T st
( x = t & p is_a_prefix_of t ) ) ;
hence contradiction ; :: thesis: verum

end;

A10: T1,{ (p ^ t1) where t1 is Element of T1 : verum } are_equipotent

proof

deffunc H₁( Element of T1) -> FinSequence of NAT = p ^ $1;
consider f being Function such that
A11: dom f = T1 and
A12: for n being Element of T1 holds f . n = H₁(n) from FUNCT_1:sch 4();
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = T1 & proj2 f = { (p ^ t1) where t1 is Element of T1 : verum } )
thus f is one-to-one :: thesis: ( proj1 f = T1 & proj2 f = { (p ^ t1) where t1 is Element of T1 : verum } )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A13: x in dom f and
A14: y in dom f and
A15: f . x = f . y ; :: thesis: x = y
reconsider m = x, n = y as Element of T1 by A11, A13, A14;
p ^ m = f . n by A12, A15
.= p ^ n by A12 ;
hence x = y by FINSEQ_1:46; :: thesis: verum

end;

thus dom f = T1 by A11; :: thesis: proj2 f = { (p ^ t1) where t1 is Element of T1 : verum }
thus rng f c= { (p ^ t1) where t1 is Element of T1 : verum } :: according to XBOOLE_0:def 10 :: thesis: { (p ^ t1) where t1 is Element of T1 : verum } c= proj2 f

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in rng f or i in { (p ^ t1) where t1 is Element of T1 : verum } )
assume i in rng f ; :: thesis: i in { (p ^ t1) where t1 is Element of T1 : verum }
then consider n being set such that
A16: n in dom f and
A17: i = f . n by FUNCT_1:def 5;
T1 c= NAT * by TREES_1:def 5;
then reconsider n = n as Element of NAT * by A11, A16;
f . n = p ^ n by A11, A12, A16;
hence i in { (p ^ t1) where t1 is Element of T1 : verum } by A11, A16, A17; :: thesis: verum

end;

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in { (p ^ t1) where t1 is Element of T1 : verum } or i in proj2 f )
assume i in { (p ^ t1) where t1 is Element of T1 : verum } ; :: thesis: i in proj2 f
then consider n being Element of T1 such that
A18: i = p ^ n ;
i = f . n by A12, A18;
hence i in proj2 f by A11, FUNCT_1:def 5; :: thesis: verum

end;

then reconsider C = { (p ^ t1) where t1 is Element of T1 : verum } as finite set by CARD_1:68;
A19: card T1 = card C by A10, CARD_1:21;
T | p,B are_equipotent by Th13;
then card (T | p) = card B by CARD_1:21;
hence (card (T with-replacement p,T1)) + (card (T | p)) = ((card A) + (card C)) + (card B) by A3, A4, CARD_2:53
.= ((card A) + (card B)) + (card C)
.= (card T) + (card T1) by A7, A8, A19, CARD_2:53 ;
:: thesis: verum