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 Def9;
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 object ; :: 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 Th18;
p ^ q in T with-replacement (p,T1) by A1, A3, Def9;
hence x in (T with-replacement (p,T1)) | p by A2, Def6; :: thesis: verum
end;
let x be object ; :: 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 Th18;
A5: p ^ q in T with-replacement (p,T1) by A2, A4, Def6;
A6: now :: thesis: ( p ^ q in T & not p is_a_proper_prefix_of p ^ q implies q in T1 )
assume that
p ^ q in T and
A7: not p is_a_proper_prefix_of p ^ q ; :: thesis: q in T1
p is_a_prefix_of p ^ q by Th1;
then p ^ q = p by A7
.= p ^ {} by FINSEQ_1:34 ;
then q = {} by FINSEQ_1:33;
hence q in T1 by Th21; :: thesis: verum
end;
( ex r being FinSequence of NAT st
( r in T1 & p ^ q = p ^ r ) implies q in T1 ) by FINSEQ_1:33;
hence x in T1 by A1, A5, A6, Def9; :: thesis: verum