let T be finite Tree; :: thesis: for p being Element of T holds T | p, { t where t is Element of T : p is_a_prefix_of t } are_equipotent
let p be Element of T; :: thesis: T | p, { t where t is Element of T : p is_a_prefix_of t } are_equipotent
set X = { t where t is Element of T : p is_a_prefix_of t } ;
deffunc H₁( Element of T | p) -> FinSequence of NAT = p ^ $1;
consider f being Function such that
A1: dom f = T | p and
A2: 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 = { t where t is Element of T : p is_a_prefix_of t } )
thus f is one-to-one :: thesis: ( proj1 f = T | p & proj2 f = { t where t is Element of T : p is_a_prefix_of t } )

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
A3: ( x in dom f & y in dom f ) and
A4: f . x = f . y ; :: thesis: x = y
reconsider m = x, n = y as Element of T | p by A1, A3;
p ^ m = f . n by A2, A4
.= p ^ n by A2 ;
hence x = y by FINSEQ_1:33; :: thesis: verum

end;

thus dom f = T | p by A1; :: thesis: proj2 f = { t where t is Element of T : p is_a_prefix_of t }
thus rng f c= { t where t is Element of T : p is_a_prefix_of t } :: according to XBOOLE_0:def 10 :: thesis: { t where t is Element of T : p is_a_prefix_of t } c= proj2 f

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng f or i in { t where t is Element of T : p is_a_prefix_of t } )
assume i in rng f ; :: thesis: i in { t where t is Element of T : p is_a_prefix_of t }
then consider n being object such that
A5: n in dom f and
A6: i = f . n by FUNCT_1:def 3;
reconsider n = n as Element of T | p by A1, A5;
reconsider t = p ^ n as Element of T by TREES_1:def 6;
( f . n = p ^ n & p is_a_prefix_of t ) by A2, TREES_1:1;
hence i in { t where t is Element of T : p is_a_prefix_of t } by A6; :: thesis: verum

end;

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in { t where t is Element of T : p is_a_prefix_of t } or i in proj2 f )
assume i in { t where t is Element of T : p is_a_prefix_of t } ; :: thesis: i in proj2 f
then A7: ex t being Element of T st
( i = t & p is_a_prefix_of t ) ;
then consider n being FinSequence such that
A8: i = p ^ n by TREES_1:1;
n is FinSequence of NAT by A7, A8, FINSEQ_1:36;
then reconsider n = n as Element of T | p by A7, A8, TREES_1:def 6;
i = f . n by A2, A8;
hence i in proj2 f by A1, FUNCT_1:def 3; :: thesis: verum