let p be FinSequence of NAT ; :: thesis: for T, T1 being Tree st p in T holds
T with-replacement (p,T1) = { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : s = s }
let T, T1 be Tree; :: thesis: ( p in T implies T with-replacement (p,T1) = { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : s = s } )
assume A1: p in T ; :: thesis: T with-replacement (p,T1) = { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : s = s }
thus T with-replacement (p,T1) c= { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : s = s } :: according to XBOOLE_0:def 10 :: thesis: { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : s = s } is_a_prefix_of T with-replacement (p,T1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T with-replacement (p,T1) or x in { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : s = s } )
assume A2: x in T with-replacement (p,T1) ; :: thesis: x in { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : s = s }
then reconsider q = x as FinSequence of NAT by Th44;
A3: ( ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) implies x in { (p ^ s) where s is Element of T1 : s = s } ) ;
( q in T & not p is_a_proper_prefix_of q implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } ) ;
hence x in { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : s = s } by A1, A2, A3, Def12, XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : s = s } or x in T with-replacement (p,T1) )
assume A4: x in { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : s = s } ; :: thesis: x in T with-replacement (p,T1)

A5: now

assume x in { (p ^ s) where s is Element of T1 : s = s } ; :: thesis: x in T with-replacement (p,T1)
then ex s being Element of T1 st
( x = p ^ s & s = s ) ;
hence x in T with-replacement (p,T1) by A1, Def12; :: thesis: verum

end;

now

assume x in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis: x in T with-replacement (p,T1)
then ex t being Element of T st
( x = t & not p is_a_proper_prefix_of t ) ;
hence x in T with-replacement (p,T1) by A1, Def12; :: thesis: verum

end;

hence x in T with-replacement (p,T1) by A4, A5, XBOOLE_0:def 3; :: thesis: verum