let T be finite Tree; :: thesis:
let p be Element of T; :: thesis:
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

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:
thus f is one-to-one :: thesis:

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A4: ( x in dom f & y in dom f ) and
A5: f . x = f . y ; :: thesis:
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:

end;

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

let i be object ; :: according to TARSKI:def 3 :: thesis:
assume i in rng f ; :: thesis:
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:

end;

let i be object ; :: according to TARSKI:def 3 :: thesis:
assume i in { (p9 ^ n) where n is Element of NAT * : n in T | p } ; :: thesis:
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:

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:
A12: X <> T

end;

X c= T

end;