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_{1}[ Element of T] means not p is_a_prefix_of $1;

defpred S_{2}[ Element of T] means p is_a_prefix_of $1;

set A = { t where t is Element of T : S_{1}[t] } ;

set B = { t where t is Element of T : S_{2}[t] } ;

set C = { (p ^ t1) where t1 is Element of T1 : verum } ;

A1: { t where t is Element of T : S_{1}[t] } is Subset of T
from DOMAIN_1:sch 7();

A2: { t where t is Element of T : S_{2}[t] } is Subset of T
from DOMAIN_1:sch 7();

A3: T1, { (p ^ t1) where t1 is Element of T1 : verum } are_equipotent_{1}[t] } , B = { t where t is Element of T : S_{2}[t] } as finite set by A1, A2;

A12: A misses { (p ^ t1) where t1 is Element of T1 : verum }

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

let p be Element of T; :: thesis: (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)

defpred S

defpred S

set A = { t where t is Element of T : S

set B = { t where t is Element of T : S

set C = { (p ^ t1) where t1 is Element of T1 : verum } ;

A1: { t where t is Element of T : S

A2: { t where t is Element of T : S

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

proof

reconsider A = { t where t is Element of T : S
deffunc H_{1}( 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_{1}(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 } )

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

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;consider f being Function such that

A4: dom f = T1 and

A5: for n being Element of T1 holds f . n = H

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

thus
dom f = T1
by A4; :: thesis: proj2 f = { (p ^ t1) where t1 is Element of T1 : verum }
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;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

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 { (p ^ t1) where t1 is Element of T1 : verum } or i in proj2 f )
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;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

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

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 ) )

then A11:
T = A \/ B
by XBOOLE_0:def 3;( ( 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 ) )

hence x in T by A1, A2; :: thesis: verum

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

assume
( x in A or x in B )
; :: thesis: x in Tassume
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;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

hence x in T by A1, A2; :: thesis: verum

A12: A misses { (p ^ t1) where t1 is Element of T1 : verum }

proof

A15:
A misses B
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;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

proof

A18:
T with-replacement (p,T1) = A \/ { (p ^ t1) where t1 is Element of T1 : verum }
by Th9;
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;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

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