let T, T1 be finite Tree; :: thesis: for p being Element of T holds T with-replacement (p,T1) = { t where t is Element of T : not p is_a_prefix_of t } \/ { (p ^ t1) where t1 is Element of T1 : verum }

let p be Element of T; :: thesis: T with-replacement (p,T1) = { t where t is Element of T : not p is_a_prefix_of t } \/ { (p ^ t1) where t1 is Element of T1 : verum }

defpred S_{1}[ set ] means verum;

defpred S_{2}[ set ] means $1 = $1;

deffunc H_{1}( FinSequence) -> set = p ^ $1;

set A = { t where t is Element of T : not p is_a_proper_prefix_of t } ;

set B = { H_{1}(t1) where t1 is Element of T1 : S_{2}[t1] } ;

set C = { t where t is Element of T : not p is_a_prefix_of t } ;

set D = { H_{1}(t1) where t1 is Element of T1 : S_{1}[t1] } ;

( {} is Element of T1 & p ^ {} = p ) by FINSEQ_1:34, TREES_1:22;

then A6: p in { H_{1}(t1) where t1 is Element of T1 : S_{1}[t1] }
;

thus T with-replacement (p,T1) = ( { t where t is Element of T : not p is_a_prefix_of t } \/ {p}) \/ { H_{1}(t1) where t1 is Element of T1 : S_{1}[t1] }
by A5, TREES_1:32

.= { t where t is Element of T : not p is_a_prefix_of t } \/ ({p} \/ { H_{1}(t1) where t1 is Element of T1 : S_{1}[t1] } )
by XBOOLE_1:4

.= { t where t is Element of T : not p is_a_prefix_of t } \/ { H_{1}(t1) where t1 is Element of T1 : S_{1}[t1] }
by A6, ZFMISC_1:40
; :: thesis: verum

let p be Element of T; :: thesis: T with-replacement (p,T1) = { t where t is Element of T : not p is_a_prefix_of t } \/ { (p ^ t1) where t1 is Element of T1 : verum }

defpred S

defpred S

deffunc H

set A = { t where t is Element of T : not p is_a_proper_prefix_of t } ;

set B = { H

set C = { t where t is Element of T : not p is_a_prefix_of t } ;

set D = { H

now :: thesis: for x being object holds

( ( not x in { t where t is Element of T : not p is_a_proper_prefix_of t } or x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) & ( ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } ) )

then A5:
{ t where t is Element of T : not p is_a_proper_prefix_of t } = { t where t is Element of T : not p is_a_prefix_of t } \/ {p}
by XBOOLE_0:def 3;( ( not x in { t where t is Element of T : not p is_a_proper_prefix_of t } or x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) & ( ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } ) )

let x be object ; :: thesis: ( ( not x in { t where t is Element of T : not p is_a_proper_prefix_of t } or x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) & ( ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } ) )

then ( x = p or ex t being Element of T st

( t = x & not p is_a_prefix_of t ) ) by TARSKI:def 1;

then consider t being Element of T such that

A3: t = x and

A4: ( t = p or not p is_a_prefix_of t ) ;

not p is_a_proper_prefix_of t by A4;

hence x in { t where t is Element of T : not p is_a_proper_prefix_of t } by A3; :: thesis: verum

end;hereby :: thesis: ( ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } )

assume
( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} )
; :: thesis: x in { t where t is Element of T : not p is_a_proper_prefix_of t } assume
x in { t where t is Element of T : not p is_a_proper_prefix_of t }
; :: thesis: ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} )

then consider t being Element of T such that

A1: x = t and

A2: not p is_a_proper_prefix_of t ;

( not p is_a_prefix_of t or t = p ) by A2;

hence ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) by A1, TARSKI:def 1; :: thesis: verum

end;then consider t being Element of T such that

A1: x = t and

A2: not p is_a_proper_prefix_of t ;

( not p is_a_prefix_of t or t = p ) by A2;

hence ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) by A1, TARSKI:def 1; :: thesis: verum

then ( x = p or ex t being Element of T st

( t = x & not p is_a_prefix_of t ) ) by TARSKI:def 1;

then consider t being Element of T such that

A3: t = x and

A4: ( t = p or not p is_a_prefix_of t ) ;

not p is_a_proper_prefix_of t by A4;

hence x in { t where t is Element of T : not p is_a_proper_prefix_of t } by A3; :: thesis: verum

( {} is Element of T1 & p ^ {} = p ) by FINSEQ_1:34, TREES_1:22;

then A6: p in { H

thus T with-replacement (p,T1) = ( { t where t is Element of T : not p is_a_prefix_of t } \/ {p}) \/ { H

.= { t where t is Element of T : not p is_a_prefix_of t } \/ ({p} \/ { H

.= { t where t is Element of T : not p is_a_prefix_of t } \/ { H