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 :: thesis: for q being FinSequence of NAT holds
( ( q in W implies q in W with-replacement (p,(W | p)) ) & ( q in W with-replacement (p,(W | p)) implies q in W ) )
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 :: thesis: ( p is_a_proper_prefix_of q implies ex r being FinSequence of NAT st
( r in W | p & q = p ^ r ) )
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 ;
then consider r being FinSequence such that
A3: q = p ^ r by TREES_1:1;
rng r c= rng q by A3, FINSEQ_1:30;
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 6; :: thesis: verum
end;
hence q in W with-replacement (p,(W | p)) by A1, A2, TREES_1:def 9; :: thesis: verum
end;
assume that
A4: q in W with-replacement (p,(W | p)) and
A5: not q in W ; :: thesis: contradiction
ex r being FinSequence of NAT st
( r in W | p & q = p ^ r ) by A1, A4, A5, TREES_1:def 9;
hence contradiction by A1, A5, TREES_1:def 6; :: thesis: verum
end;
hence W = W with-replacement (p,(W | p)) ; :: thesis: verum