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_{1}( 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_{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 = { 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 } )

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

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

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

consider f being Function such that

A1: dom f = T | p and

A2: 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 = { 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

thus
dom f = T | p
by A1; :: thesis: proj2 f = { t where t is Element of T : p is_a_prefix_of t }
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;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

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 { t where t is Element of T : p is_a_prefix_of t } or i in proj2 f )
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;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

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