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 )
assume A1: p <> {} ; :: thesis: card (T | p) < card T
reconsider p' = p as Element of NAT * by FINSEQ_1:def 11;
set X = { (p' ^ n) where n is Element of NAT * : n in T | p } ;
A2: T | p,{ (p' ^ n) where n is Element of NAT * : n in T | p } are_equipotent

proof

deffunc H₁( Element of T | p) -> FinSequence of NAT = p' ^ $1;
consider f being Function such that
A3: dom f = T | p and
A4: for n being Element of T | p 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 = T | p & proj2 f = { (p' ^ n) where n is Element of NAT * : n in T | p } )
thus f is one-to-one :: thesis: ( proj1 f = T | p & proj2 f = { (p' ^ n) where n is Element of NAT * : n in T | p } )

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
A5: x in dom f and
A6: y in dom f and
A7: f . x = f . y ; :: thesis: x = y
reconsider m = x, n = y as Element of T | p by A3, A5, A6;
p' ^ m = f . n by A4, A7
.= p' ^ n by A4 ;
hence x = y by FINSEQ_1:46; :: thesis: verum

end;

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

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in rng f or i in { (p' ^ n) where n is Element of NAT * : n in T | p } )
assume i in rng f ; :: thesis: i in { (p' ^ n) where n is Element of NAT * : n in T | p }
then consider n being set such that
A8: n in dom f and
A9: i = f . n by FUNCT_1:def 5;
T | p c= NAT * by TREES_1:def 5;
then reconsider n = n as Element of NAT * by A3, A8;
f . n = p' ^ n by A3, A4, A8;
hence i in { (p' ^ n) where n is Element of NAT * : n in T | p } by A3, A8, A9; :: thesis: verum

end;

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in { (p' ^ n) where n is Element of NAT * : n in T | p } or i in proj2 f )
assume i in { (p' ^ 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
A10: i = p' ^ n and
A11: n in T | p ;
reconsider n = n as Element of T | p by A11;
i = f . n by A4, A10;
hence i in proj2 f by A3, FUNCT_1:def 5; :: thesis: verum

end;

then reconsider X = { (p' ^ n) where n is Element of NAT * : n in T | p } as finite set by CARD_1:68;
A12: X c= T

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in X or i in T )
assume i in X ; :: thesis: i in T
then consider n being Element of NAT * such that
A13: ( i = p' ^ n & n in T | p ) ;
thus i in T by A13, TREES_1:def 9; :: thesis: verum

end;

X <> T

proof

assume X = T ; :: thesis: contradiction
then {} in X by TREES_1:47;
then ex n being Element of NAT * st
( {} = p' ^ n & n in T | p ) ;
hence contradiction by A1; :: thesis: verum

end;

then A14: X c< T by A12, XBOOLE_0:def 8;
card X = card (T | p) by A2, CARD_1:21;
hence card (T | p) < card T by A14, CARD_2:67; :: thesis: verum