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

proof

deffunc H₁( 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₁(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 } )

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

thus dom f = T | p by A2; :: thesis: 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

proof

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;

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

then reconsider X = { (p9 ^ n) where n is Element of NAT * : n in T | p } as finite set by CARD_1:38;
A10: card X = card (T | p) by A1, CARD_1:5;
assume A11: p <> {} ; :: thesis: card (T | p) < card T
A12: X <> T

proof

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;

X c= T

proof

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;

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