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 )

proof

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

A2: now

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;

now

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;

hence p in T with-replacement t,T1 by A1, A2, Def1, TREES_1:def 12; :: thesis: verum

end;

assume A5: p in T with-replacement t,T1 ; :: thesis: 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;

now

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

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;

end;

hence p in tree T,{t},T1 by A5, A6, Def1, TREES_1:def 12; :: thesis: verum