defpred S₁[ FinSequence, set ] means ( ( not p is_a_prefix_of $1 & $2 = T . $1 ) or ex r being FinSequence of NAT st
( r in dom T1 & $1 = p ^ r & $2 = T1 . r ) );
A2: for q being FinSequence of NAT st q in (dom T) with-replacement (p,(dom T1)) holds
ex x being set st S₁[q,x]

proof

let q be FinSequence of NAT ; :: thesis: ( q in (dom T) with-replacement (p,(dom T1)) implies ex x being set st S₁[q,x] )
assume A3: q in (dom T) with-replacement (p,(dom T1)) ; :: thesis: ex x being set st S₁[q,x]

now :: thesis: ex x being set st S₁[q,x]

per cases ( p is_a_proper_prefix_of q or p = q or not p is_a_prefix_of q ) ;

suppose p is_a_proper_prefix_of q ; :: thesis: ex x being set st S₁[q,x]

then consider r being FinSequence of NAT such that
A4: ( r in dom T1 & q = p ^ r ) by A1, A3, TREES_1:def 9;
thus ex x being set st S₁[q,x] :: thesis: verum

proof

take T1 . r ; :: thesis: S₁[q,T1 . r]
thus S₁[q,T1 . r] by A4; :: thesis: verum

end;

end;

suppose A5: p = q ; :: thesis: ex x being set st S₁[q,x]

thus ex x being set st S₁[q,x] :: thesis: verum

proof

take T1 . ({} NAT) ; :: thesis: S₁[q,T1 . ({} NAT)]
( {} NAT in dom T1 & q = p ^ (<*> NAT) ) by A5, FINSEQ_1:34, TREES_1:22;
hence S₁[q,T1 . ({} NAT)] ; :: thesis: verum

end;

end;

suppose not p is_a_prefix_of q ; :: thesis: ex x being set st S₁[q,x]

hence ex x being set st S₁[q,x] ; :: thesis: verum

end;

end;

end;

hence ex x being set st S₁[q,x] ; :: thesis: verum

end;

thus ex TT being DecoratedTree st
( dom TT = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT st q in (dom T) with-replacement (p,(dom T1)) holds
S₁[q,TT . q] ) ) from TREES_2:sch 6(A2); :: thesis: verum