let T be finite Tree; :: thesis: for p being Element of T st p <> {} holds

card (T | p) < card T

let p be Element of T; :: thesis: ( p <> {} implies card (T | p) < card T )

reconsider p9 = p as Element of NAT * by FINSEQ_1:def 11;

set X = { (p9 ^ n) where n is Element of NAT * : n in T | p } ;

A1: T | p, { (p9 ^ n) where n is Element of NAT * : n in T | p } are_equipotent

A10: card X = card (T | p) by A1, CARD_1:5;

assume A11: p <> {} ; :: thesis: card (T | p) < card T

A12: X <> T

hence card (T | p) < card T by A10, CARD_2:48; :: thesis: verum

card (T | p) < card T

let p be Element of T; :: thesis: ( p <> {} implies card (T | p) < card T )

reconsider p9 = p as Element of NAT * by FINSEQ_1:def 11;

set X = { (p9 ^ n) where n is Element of NAT * : n in T | p } ;

A1: T | p, { (p9 ^ n) where n is Element of NAT * : n in T | p } are_equipotent

proof

then reconsider X = { (p9 ^ n) where n is Element of NAT * : n in T | p } as finite set by CARD_1:38;
deffunc H_{1}( Element of T | p) -> FinSequence of NAT = p9 ^ $1;

consider f being Function such that

A2: dom f = T | p and

A3: for n being Element of T | p 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 = T | p & proj2 f = { (p9 ^ n) where n is Element of NAT * : n in T | p } )

thus f is one-to-one :: thesis: ( proj1 f = T | p & proj2 f = { (p9 ^ n) where n is Element of NAT * : n in T | p } )

thus rng f c= { (p9 ^ n) where n is Element of NAT * : n in T | p } :: according to XBOOLE_0:def 10 :: thesis: { (p9 ^ n) where n is Element of NAT * : n in T | p } c= proj2 f

assume i in { (p9 ^ n) where n is Element of NAT * : n in T | p } ; :: thesis: i in proj2 f

then consider n being Element of NAT * such that

A8: i = p9 ^ n and

A9: n in T | p ;

reconsider n = n as Element of T | p by A9;

i = f . n by A3, A8;

hence i in proj2 f by A2, FUNCT_1:def 3; :: thesis: verum

end;consider f being Function such that

A2: dom f = T | p and

A3: for n being Element of T | p holds f . n = H

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = T | p & proj2 f = { (p9 ^ n) where n is Element of NAT * : n in T | p } )

thus f is one-to-one :: thesis: ( proj1 f = T | p & proj2 f = { (p9 ^ n) where n is Element of NAT * : n in T | p } )

proof

thus
dom f = T | p
by A2; :: thesis: proj2 f = { (p9 ^ n) where n is Element of NAT * : n in T | p }
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

A4: ( x in dom f & y in dom f ) and

A5: f . x = f . y ; :: thesis: x = y

reconsider m = x, n = y as Element of T | p by A2, A4;

p9 ^ m = f . n by A3, A5

.= p9 ^ n by A3 ;

hence x = y by FINSEQ_1:33; :: thesis: verum

end;assume that

A4: ( x in dom f & y in dom f ) and

A5: f . x = f . y ; :: thesis: x = y

reconsider m = x, n = y as Element of T | p by A2, A4;

p9 ^ m = f . n by A3, A5

.= p9 ^ n by A3 ;

hence x = y by FINSEQ_1:33; :: thesis: verum

thus rng f c= { (p9 ^ n) where n is Element of NAT * : n in T | p } :: according to XBOOLE_0:def 10 :: thesis: { (p9 ^ n) where n is Element of NAT * : n in T | p } c= proj2 f

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in { (p9 ^ n) where n is Element of NAT * : n in T | p } or i in proj2 f )
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng f or i in { (p9 ^ n) where n is Element of NAT * : n in T | p } )

assume i in rng f ; :: thesis: i in { (p9 ^ n) where n is Element of NAT * : n in T | p }

then consider n being object such that

A6: n in dom f and

A7: i = f . n by FUNCT_1:def 3;

T | p c= NAT * by TREES_1:def 3;

then reconsider n = n as Element of NAT * by A2, A6;

f . n = p9 ^ n by A2, A3, A6;

hence i in { (p9 ^ n) where n is Element of NAT * : n in T | p } by A2, A6, A7; :: thesis: verum

end;assume i in rng f ; :: thesis: i in { (p9 ^ n) where n is Element of NAT * : n in T | p }

then consider n being object such that

A6: n in dom f and

A7: i = f . n by FUNCT_1:def 3;

T | p c= NAT * by TREES_1:def 3;

then reconsider n = n as Element of NAT * by A2, A6;

f . n = p9 ^ n by A2, A3, A6;

hence i in { (p9 ^ n) where n is Element of NAT * : n in T | p } by A2, A6, A7; :: thesis: verum

assume i in { (p9 ^ n) where n is Element of NAT * : n in T | p } ; :: thesis: i in proj2 f

then consider n being Element of NAT * such that

A8: i = p9 ^ n and

A9: n in T | p ;

reconsider n = n as Element of T | p by A9;

i = f . n by A3, A8;

hence i in proj2 f by A2, FUNCT_1:def 3; :: thesis: verum

A10: card X = card (T | p) by A1, CARD_1:5;

assume A11: p <> {} ; :: thesis: card (T | p) < card T

A12: X <> T

proof

X c= T
assume
X = T
; :: thesis: contradiction

then {} in X by TREES_1:22;

then ex n being Element of NAT * st

( {} = p9 ^ n & n in T | p ) ;

hence contradiction by A11; :: thesis: verum

end;then {} in X by TREES_1:22;

then ex n being Element of NAT * st

( {} = p9 ^ n & n in T | p ) ;

hence contradiction by A11; :: thesis: verum

proof

then
X c< T
by A12;
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in X or i in T )

assume i in X ; :: thesis: i in T

then ex n being Element of NAT * st

( i = p9 ^ n & n in T | p ) ;

hence i in T by TREES_1:def 6; :: thesis: verum

end;assume i in X ; :: thesis: i in T

then ex n being Element of NAT * st

( i = p9 ^ n & n in T | p ) ;

hence i in T by TREES_1:def 6; :: thesis: verum

hence card (T | p) < card T by A10, CARD_2:48; :: thesis: verum