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 }

proof

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;

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;
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