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)

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)

now

assume p is_a_proper_prefix_of q ; :: thesis: ex r being FinSequence of NAT st
( r in W | p & q = p ^ r )
then p is_a_prefix_of q by XBOOLE_0:def 8;
then consider r being FinSequence such that
A7: q = p ^ r by TREES_1:8;
rng r c= rng q by A7, FINSEQ_1:43;
then rng r c= NAT by XBOOLE_1:1;
then reconsider r = r as FinSequence of NAT by 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;

hence q in W with-replacement p,(W | p) by A1, A3, 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
ex r being FinSequence of NAT st
( r in W | p & q = p ^ r ) by A1, A10, A11, TREES_1:def 12;
hence contradiction by A1, A11, TREES_1:def 9; :: thesis: verum

end;

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