let T, T1 be finite Tree; :: thesis: for p being Element of T

for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds

ex t1 being Element of T1 st f = p ^ t1

let p be Element of T; :: thesis: for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds

ex t1 being Element of T1 st f = p ^ t1

let f be FinSequence of NAT ; :: thesis: ( f in T with-replacement (p,T1) & p is_a_prefix_of f implies ex t1 being Element of T1 st f = p ^ t1 )

assume that

A1: f in T with-replacement (p,T1) and

A2: p is_a_prefix_of f ; :: thesis: ex t1 being Element of T1 st f = p ^ t1

A3: not f in { t where t is Element of T : not p is_a_prefix_of t }

then f in { (p ^ t1) where t1 is Element of T1 : verum } by A1, A3, XBOOLE_0:def 3;

hence ex t1 being Element of T1 st f = p ^ t1 ; :: thesis: verum

for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds

ex t1 being Element of T1 st f = p ^ t1

let p be Element of T; :: thesis: for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds

ex t1 being Element of T1 st f = p ^ t1

let f be FinSequence of NAT ; :: thesis: ( f in T with-replacement (p,T1) & p is_a_prefix_of f implies ex t1 being Element of T1 st f = p ^ t1 )

assume that

A1: f in T with-replacement (p,T1) and

A2: p is_a_prefix_of f ; :: thesis: ex t1 being Element of T1 st f = p ^ t1

A3: not f in { t where t is Element of T : not p is_a_prefix_of t }

proof

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 }
by Th9;
assume
f in { t where t is Element of T : not p is_a_prefix_of t }
; :: thesis: contradiction

then ex t being Element of T st

( f = t & not p is_a_prefix_of t ) ;

hence contradiction by A2; :: thesis: verum

end;then ex t being Element of T st

( f = t & not p is_a_prefix_of t ) ;

hence contradiction by A2; :: thesis: verum

then f in { (p ^ t1) where t1 is Element of T1 : verum } by A1, A3, XBOOLE_0:def 3;

hence ex t1 being Element of T1 st f = p ^ t1 ; :: thesis: verum