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();
A3: 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
A4: dom f = T1 and
A5: 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, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A6: ( x in dom f & y in dom f ) and
A7: f . x = f . y ; :: thesis: x = y
reconsider m = x, n = y as Element of T1 by A4, A6;
p ^ m = f . n by A5, A7
.= p ^ n by A5 ;
hence x = y by FINSEQ_1:33; :: thesis: verum

end;

thus dom f = T1 by A4; :: 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 object ; :: 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 object such that
A8: n in dom f and
A9: i = f . n by FUNCT_1:def 3;
T1 c= NAT * by TREES_1:def 3;
then reconsider n = n as Element of NAT * by A4, A8;
f . n = p ^ n by A4, A5, A8;
hence i in { (p ^ t1) where t1 is Element of T1 : verum } by A4, A8, A9; :: thesis: verum

end;

let i be object ; :: 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
A10: i = p ^ n ;
i = f . n by A5, A10;
hence i in proj2 f by A4, FUNCT_1:def 3; :: thesis: verum

end;

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, A2;

now :: thesis: for x being object holds
( ( not x in T or x in A or x in B ) & ( ( x in A or x in B ) implies x in T ) )

let x be object ; :: 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 A11: T = A \/ B by XBOOLE_0:def 3;
A12: 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 object such that
A13: x in A /\ { (p ^ t1) where t1 is Element of T1 : verum } by XBOOLE_0:4;
x in { (p ^ t1) where t1 is Element of T1 : verum } by A13, XBOOLE_0:def 4;
then A14: ex t1 being Element of T1 st x = p ^ t1 ;
x in A by A13, XBOOLE_0:def 4;
then ex t being Element of T st
( x = t & not p is_a_prefix_of t ) ;
hence contradiction by A14, TREES_1:1; :: thesis: verum

end;

A15: A misses B

proof

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

end;

A18: T with-replacement (p,T1) = A \/ { (p ^ t1) where t1 is Element of T1 : verum } by Th9;
reconsider C = { (p ^ t1) where t1 is Element of T1 : verum } as finite set by A3, CARD_1:38;
A19: card T1 = card C by A3, CARD_1:5;
T | p,B are_equipotent by Th8;
then card (T | p) = card B by CARD_1:5;
hence (card (T with-replacement (p,T1))) + (card (T | p)) = ((card A) + (card C)) + (card B) by A18, A12, CARD_2:40
.= ((card A) + (card B)) + (card C)
.= (card T) + (card T1) by A11, A15, A19, CARD_2:40 ;
:: thesis: verum