let T, T1 be finite Tree; :: thesis: for p being Element of T holds T with-replacement (p,T1) = { t where t is Element of T : not p is_a_prefix_of t } \/ { (p ^ t1) where t1 is Element of T1 : verum }
let p be Element of T; :: thesis: T with-replacement (p,T1) = { t where t is Element of T : not p is_a_prefix_of t } \/ { (p ^ t1) where t1 is Element of T1 : verum }
defpred S1[ set ] means verum;
defpred S2[ set ] means $1 = $1;
deffunc H1( FinSequence) -> set = p ^ $1;
set A = { t where t is Element of T : not p is_a_proper_prefix_of t } ;
set B = { H1(t1) where t1 is Element of T1 : S2[t1] } ;
set C = { t where t is Element of T : not p is_a_prefix_of t } ;
set D = { H1(t1) where t1 is Element of T1 : S1[t1] } ;
now :: thesis: for x being object holds
( ( not x in { t where t is Element of T : not p is_a_proper_prefix_of t } or x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) & ( ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } ) )
let x be object ; :: thesis: ( ( not x in { t where t is Element of T : not p is_a_proper_prefix_of t } or x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) & ( ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } ) )
hereby :: thesis: ( ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } )
assume x in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis: ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} )
then consider t being Element of T such that
A1: x = t and
A2: not p is_a_proper_prefix_of t ;
( not p is_a_prefix_of t or t = p ) by A2;
hence ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) by A1, TARSKI:def 1; :: thesis: verum
end;
assume ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) ; :: thesis: x in { t where t is Element of T : not p is_a_proper_prefix_of t }
then ( x = p or ex t being Element of T st
( t = x & not p is_a_prefix_of t ) ) by TARSKI:def 1;
then consider t being Element of T such that
A3: t = x and
A4: ( t = p or not p is_a_prefix_of t ) ;
not p is_a_proper_prefix_of t by A4;
hence x in { t where t is Element of T : not p is_a_proper_prefix_of t } by A3; :: thesis: verum
end;
then A5: { t where t is Element of T : not p is_a_proper_prefix_of t } = { t where t is Element of T : not p is_a_prefix_of t } \/ {p} by XBOOLE_0:def 3;
( {} is Element of T1 & p ^ {} = p ) by FINSEQ_1:34, TREES_1:22;
then A6: p in { H1(t1) where t1 is Element of T1 : S1[t1] } ;
thus T with-replacement (p,T1) = ( { t where t is Element of T : not p is_a_prefix_of t } \/ {p}) \/ { H1(t1) where t1 is Element of T1 : S1[t1] } by A5, TREES_1:32
.= { t where t is Element of T : not p is_a_prefix_of t } \/ ({p} \/ { H1(t1) where t1 is Element of T1 : S1[t1] } ) by XBOOLE_1:4
.= { t where t is Element of T : not p is_a_prefix_of t } \/ { H1(t1) where t1 is Element of T1 : S1[t1] } by A6, ZFMISC_1:40 ; :: thesis: verum