let W be Tree; :: thesis: for p being FinSequence of NAT st p in W holds
W = W with-replacement p,(W | p)
let p be FinSequence of NAT ; :: thesis: ( p in W implies W = W with-replacement p,(W | p) )
assume A1: p in W ; :: thesis: W = W with-replacement p,(W | p)

A2: now

let q be FinSequence of NAT ; :: thesis: ( ( q in W implies q in W with-replacement p,(W | p) ) & ( q in W with-replacement p,(W | p) implies q in W ) )
thus ( q in W implies q in W with-replacement p,(W | p) ) :: thesis: ( q in W with-replacement p,(W | p) implies q in W )

proof

assume A3: q in W ; :: thesis: q in W with-replacement p,(W | p)

A4: now

assume A5: p is_a_proper_prefix_of q ; :: thesis: ex r being FinSequence of NAT st
( r in W | p & q = p ^ r )
A6: p is_a_prefix_of q by A5, XBOOLE_0:def 8;
consider r being FinSequence such that
A7: q = p ^ r by A6, TREES_1:8;
A8: rng r c= rng q by A7, FINSEQ_1:43;
A9: rng r c= NAT by A8, XBOOLE_1:1;
reconsider r = r as FinSequence of NAT by A9, FINSEQ_1:def 4;
take r = r; :: thesis: ( r in W | p & q = p ^ r )
thus ( r in W | p & q = p ^ r ) by A1, A3, A7, TREES_1:def 9; :: thesis: verum

end;

thus q in W with-replacement p,(W | p) by A1, A3, A4, TREES_1:def 12; :: thesis: verum

end;

assume that
A10: q in W with-replacement p,(W | p) and
A11: not q in W ; :: thesis: contradiction
A12: ex r being FinSequence of NAT st
( r in W | p & q = p ^ r ) by A1, A10, A11, TREES_1:def 12;
thus contradiction by A1, A11, A12, TREES_1:def 9; :: thesis: verum

end;

thus W = W with-replacement p,(W | p) by A2, Th7; :: thesis: verum