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 ;
hence ex t1 being Element of T1 st f = p ^ t1 ; :: thesis: verum