let T, T1 be Tree; :: thesis: for t being Element of T holds tree (T,{t},T1) = T with-replacement (t,T1)

let t be Element of T; :: thesis: tree (T,{t},T1) = T with-replacement (t,T1)

let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in tree (T,{t},T1) or p in T with-replacement (t,T1) ) & ( not p in T with-replacement (t,T1) or p in tree (T,{t},T1) ) )

thus ( p in tree (T,{t},T1) implies p in T with-replacement (t,T1) ) :: thesis: ( not p in T with-replacement (t,T1) or p in tree (T,{t},T1) )

A6: ( p in T & not t is_a_proper_prefix_of p implies ( p in T & ( for s being FinSequence of NAT st s in {t} holds

not s is_a_proper_prefix_of p ) ) ) by TARSKI:def 1;

let t be Element of T; :: thesis: tree (T,{t},T1) = T with-replacement (t,T1)

let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in tree (T,{t},T1) or p in T with-replacement (t,T1) ) & ( not p in T with-replacement (t,T1) or p in tree (T,{t},T1) ) )

thus ( p in tree (T,{t},T1) implies p in T with-replacement (t,T1) ) :: thesis: ( not p in T with-replacement (t,T1) or p in tree (T,{t},T1) )

proof

assume A5:
p in T with-replacement (t,T1)
; :: thesis: p in tree (T,{t},T1)
assume A1:
p in tree (T,{t},T1)
; :: thesis: p in T with-replacement (t,T1)

end;A2: now :: thesis: ( p in T & ( for s being FinSequence of NAT st s in {t} holds

not s is_a_proper_prefix_of p ) implies ( p in T & not t is_a_proper_prefix_of p ) )

not s is_a_proper_prefix_of p ) implies ( p in T & not t is_a_proper_prefix_of p ) )

assume A3:
( p in T & ( for s being FinSequence of NAT st s in {t} holds

not s is_a_proper_prefix_of p ) ) ; :: thesis: ( p in T & not t is_a_proper_prefix_of p )

t in {t} by TARSKI:def 1;

hence ( p in T & not t is_a_proper_prefix_of p ) by A3; :: thesis: verum

end;not s is_a_proper_prefix_of p ) ) ; :: thesis: ( p in T & not t is_a_proper_prefix_of p )

t in {t} by TARSKI:def 1;

hence ( p in T & not t is_a_proper_prefix_of p ) by A3; :: thesis: verum

now :: thesis: ( ex s, r being FinSequence of NAT st

( s in {t} & r in T1 & p = s ^ r ) implies ex r being FinSequence of NAT st

( r in T1 & p = t ^ r ) )

hence
p in T with-replacement (t,T1)
by A1, A2, Def1, TREES_1:def 9; :: thesis: verum( s in {t} & r in T1 & p = s ^ r ) implies ex r being FinSequence of NAT st

( r in T1 & p = t ^ r ) )

given s being FinSequence of NAT such that A4:
ex r being FinSequence of NAT st

( s in {t} & r in T1 & p = s ^ r ) ; :: thesis: ex r being FinSequence of NAT st

( r in T1 & p = t ^ r )

s = t by A4, TARSKI:def 1;

hence ex r being FinSequence of NAT st

( r in T1 & p = t ^ r ) by A4; :: thesis: verum

end;( s in {t} & r in T1 & p = s ^ r ) ; :: thesis: ex r being FinSequence of NAT st

( r in T1 & p = t ^ r )

s = t by A4, TARSKI:def 1;

hence ex r being FinSequence of NAT st

( r in T1 & p = t ^ r ) by A4; :: thesis: verum

A6: ( p in T & not t is_a_proper_prefix_of p implies ( p in T & ( for s being FinSequence of NAT st s in {t} holds

not s is_a_proper_prefix_of p ) ) ) by TARSKI:def 1;

now :: thesis: ( ex r being FinSequence of NAT st

( r in T1 & p = t ^ r ) implies ex s, r being FinSequence of NAT st

( s in {t} & r in T1 & p = s ^ r ) )

hence
p in tree (T,{t},T1)
by A5, A6, Def1, TREES_1:def 9; :: thesis: verum( r in T1 & p = t ^ r ) implies ex s, r being FinSequence of NAT st

( s in {t} & r in T1 & p = s ^ r ) )

assume A7:
ex r being FinSequence of NAT st

( r in T1 & p = t ^ r ) ; :: thesis: ex s, r being FinSequence of NAT st

( s in {t} & r in T1 & p = s ^ r )

thus ex s, r being FinSequence of NAT st

( s in {t} & r in T1 & p = s ^ r ) :: thesis: verum

end;( r in T1 & p = t ^ r ) ; :: thesis: ex s, r being FinSequence of NAT st

( s in {t} & r in T1 & p = s ^ r )

thus ex s, r being FinSequence of NAT st

( s in {t} & r in T1 & p = s ^ r ) :: thesis: verum

proof

take
t
; :: thesis: ex r being FinSequence of NAT st

( t in {t} & r in T1 & p = t ^ r )

t in {t} by TARSKI:def 1;

hence ex r being FinSequence of NAT st

( t in {t} & r in T1 & p = t ^ r ) by A7; :: thesis: verum

end;( t in {t} & r in T1 & p = t ^ r )

t in {t} by TARSKI:def 1;

hence ex r being FinSequence of NAT st

( t in {t} & r in T1 & p = t ^ r ) by A7; :: thesis: verum