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
A2: p in T with-replacement p,T1 by A1, 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
reconsider q = x as FinSequence of NAT by A3, Th44;
A4: p ^ q in T with-replacement p,T1 by A1, A3, Def12;
thus x in (T with-replacement p,T1) | p by A2, A4, 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 A5: x in (T with-replacement p,T1) | p ; :: thesis: x in T1
reconsider q = x as FinSequence of NAT by A5, Th44;
A6: p ^ q in T with-replacement p,T1 by A2, A5, Def9;

A7: now

assume that
p ^ q in T and
A8: not p is_a_proper_prefix_of p ^ q ; :: thesis: q in T1
A9: p is_a_prefix_of p ^ q by Th8;
A10: p ^ q = p by A8, A9, XBOOLE_0:def 8
.= p ^ {} by FINSEQ_1:47 ;
A11: q = {} by A10, FINSEQ_1:46;
thus q in T1 by A11, Th47; :: thesis: verum

end;

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