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 A2: 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
A3: q = p ^ r by TREES_1:8;
( rng r c= rng q & rng q c= NAT ) by A3, 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, A2, A3, TREES_1:def 9; :: thesis: verum

end;

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

end;

assume A4: ( q in W with-replacement p,(W | p) & not q in W ) ; :: thesis: contradiction
then ex r being FinSequence of NAT st
( r in W | p & q = p ^ r ) by A1, TREES_1:def 12;
hence contradiction by A1, A4, TREES_1:def 9; :: thesis: verum

end;

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