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]

A4: now

per cases ( p is_a_proper_prefix_of q or p = q or not p is_a_prefix_of q ) by XBOOLE_0:def 8;

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

consider r being FinSequence of NAT such that
A6: ( r in dom T1 & q = p ^ r ) by A1, A3, A5, TREES_1:def 12;
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 A6; :: thesis: verum

end;

end;

suppose A7: 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 )]
A8: ( {} NAT in dom T1 & q = p ^ (<*> NAT ) ) by A7, FINSEQ_1:47, TREES_1:47;
thus S₁[q,T1 . ({} NAT )] by A8; :: thesis: verum

end;

end;

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

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

end;

end;

end;

thus ex x being set st S₁[q,x] by A4; :: 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