let p be FinSequence of NAT ; :: thesis: for T, T1 being Tree st p in T holds
T1 = (T with-replacement p,T1) | p
let T, T1 be Tree; :: thesis: ( p in T implies T1 = (T with-replacement p,T1) | p )
assume A1: p in T ; :: thesis: T1 = (T with-replacement p,T1) | p
then A2: p in T with-replacement p,T1 by Def12;
thus T1 c= (T with-replacement p,T1) | p :: according to XBOOLE_0:def 10 :: thesis: (T with-replacement p,T1) | p is_a_prefix_of T1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T1 or x in (T with-replacement p,T1) | p )
assume A3: x in T1 ; :: thesis: x in (T with-replacement p,T1) | p
then reconsider q = x as FinSequence of NAT by Th44;
p ^ q in T with-replacement p,T1 by A1, A3, Def12;
hence x in (T with-replacement p,T1) | p by A2, Def9; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (T with-replacement p,T1) | p or x in T1 )
assume A4: x in (T with-replacement p,T1) | p ; :: thesis: x in T1
then reconsider q = x as FinSequence of NAT by Th44;
A5: p ^ q in T with-replacement p,T1 by A2, A4, Def9;

A6: now

assume A7: ( p ^ q in T & not p is_a_proper_prefix_of p ^ q ) ; :: thesis: q in T1
p is_a_prefix_of p ^ q by Th8;
then p ^ q = p by A7, XBOOLE_0:def 8
.= p ^ {} by FINSEQ_1:47 ;
then q = {} by FINSEQ_1:46;
hence q in T1 by Th47; :: thesis: verum

end;

( ex r being FinSequence of NAT st
( r in T1 & p ^ q = p ^ r ) implies q in T1 ) by FINSEQ_1:46;
hence x in T1 by A1, A5, A6, Def12; :: thesis: verum