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₁[ set ] means $1 = $1;
defpred S₂[ set ] means verum;
deffunc H₁( FinSequence) -> set = p ^ $1;
set A = { t where t is Element of T : not p is_a_proper_prefix_of t } ;
set B = { H₁(t1) where t1 is Element of T1 : S₁[t1] } ;
set C = { t where t is Element of T : not p is_a_prefix_of t } ;
set D = { H₁(t1) where t1 is Element of T1 : S₂[t1] } ;
A1: for t1 being Element of T1 holds
( S₁[t1] iff S₂[t1] ) ;
A2: { H₁(t1) where t1 is Element of T1 : S₁[t1] } = { H₁(t1) where t1 is Element of T1 : S₂[t1] } from FRAENKEL:sch 3(A1);

now

let x be set ; :: 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 } ) )

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_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
A3: ( x = t & not p is_a_proper_prefix_of t ) ;
( not p is_a_prefix_of t or t = p ) by A3, XBOOLE_0:def 8;
hence ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) by A3, TARSKI:def 1; :: thesis: verum

end;

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 }
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
A4: t = x and
A5: ( t = p or not p is_a_prefix_of t ) ;
not p is_a_proper_prefix_of t by A5, XBOOLE_0:def 8;
hence x in { t where t is Element of T : not p is_a_proper_prefix_of t } by A4; :: thesis: verum

end;

then A6: { 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;
( {} is Element of T1 & p ^ {} = p ) by FINSEQ_1:47, TREES_1:47;
then A7: p in { H₁(t1) where t1 is Element of T1 : S₂[t1] } ;
thus T with-replacement p,T1 = ({ t where t is Element of T : not p is_a_prefix_of t } \/ {p}) \/ { H₁(t1) where t1 is Element of T1 : S₂[t1] } by A2, A6, TREES_1:64
.= { t where t is Element of T : not p is_a_prefix_of t } \/ ({p} \/ { H₁(t1) where t1 is Element of T1 : S₂[t1] } ) by XBOOLE_1:4
.= { t where t is Element of T : not p is_a_prefix_of t } \/ { H₁(t1) where t1 is Element of T1 : S₂[t1] } by A7, ZFMISC_1:46 ; :: thesis: verum