defpred S₁[ object , object , object ] means for d being DecoratedTree st d = $2 holds
$3 = F₃($1,d);
A0: for n being Nat st 1 <= n & n < len F₁() holds
for x being set ex y being set st S₁[n,x,y]

proof

let n be Nat; :: thesis: ( 1 <= n & n < len F₁() implies for x being set ex y being set st S₁[n,x,y] )
assume 1 <= n ; :: thesis: ( not n < len F₁() or for x being set ex y being set st S₁[n,x,y] )
assume n < len F₁() ; :: thesis: for x being set ex y being set st S₁[n,x,y]
let x be set ; :: thesis: ex y being set st S₁[n,x,y]

per cases ( x is DecoratedTree or not x is DecoratedTree ) ;

suppose x is DecoratedTree ; :: thesis: ex y being set st S₁[n,x,y]

then reconsider xx = x as DecoratedTree ;
take y = F₃(n,xx); :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

suppose A4: x is not DecoratedTree ; :: thesis: ex y being set st S₁[n,x,y]

take y = 0 ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] by A4; :: thesis: verum

end;

end;

end;

consider p being FinSequence such that
A1: ( len p = len F₁() & ( p . 1 = F₂() or len F₁() = 0 ) & ( for i being natural set st 1 <= i & i < len F₁() holds
S₁[i,p . i,p . (i + 1)] ) ) from RECDEF_1:sch 3(A0);
reconsider p = p as non empty FinSequence by A1;
p is DTree-yielding

proof

let a be object ; :: according to TREES_3:def 5,TREES_3:def 11 :: thesis: ( not a in proj2 p or a is set )
assume a in rng p ; :: thesis: a is set
then consider b being object such that
A5: ( b in dom p & a = p . b ) by FUNCT_1:def 3;
reconsider b = b as Element of dom F₁() by A5, A1, FINSEQ_3:29;
defpred S₂[ Nat] means ( $1 in dom F₁() implies p . $1 is DecoratedTree );
A6: S₂[1] by A1;
A7: for i being Nat st i >= 1 & S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( i >= 1 & S₂[i] implies S₂[i + 1] )
assume A8: ( i >= 1 & S₂[i] & i + 1 in dom F₁() ) ; :: thesis: p . (i + 1) is DecoratedTree
then AC: i + 1 <= len F₁() by FINSEQ_3:25;
then i < len F₁() by NAT_1:13;
then reconsider px = p . i as DecoratedTree by A8, FINSEQ_3:25;
p . (i + 1) = F₃(i,px) by A1, A8, AC, NAT_1:13;
hence p . (i + 1) is DecoratedTree ; :: thesis: verum

end;

for i being Nat st i >= 1 holds
S₂[i] from NAT_1:sch 8(A6, A7);
then ( b >= 1 implies a is DecoratedTree ) by A5;
hence a is set by FINSEQ_3:25; :: thesis: verum

end;

then reconsider p = p as non empty DTree-yielding FinSequence ;
take p ; :: thesis: ( dom p = dom F₁() & p . 1 = F₂() & ( for i, j being Element of dom F₁() st j = i + 1 holds
for d being DecoratedTree st d = p . i holds
p . j = F₃(i,d) ) )
thus dom p = dom F₁() by A1, FINSEQ_3:29; :: thesis: ( p . 1 = F₂() & ( for i, j being Element of dom F₁() st j = i + 1 holds
for d being DecoratedTree st d = p . i holds
p . j = F₃(i,d) ) )
thus p . 1 = F₂() by A1; :: thesis: for i, j being Element of dom F₁() st j = i + 1 holds
for d being DecoratedTree st d = p . i holds
p . j = F₃(i,d)
let i, j be Element of dom F₁(); :: thesis: ( j = i + 1 implies for d being DecoratedTree st d = p . i holds
p . j = F₃(i,d) )
assume A3: j = i + 1 ; :: thesis: for d being DecoratedTree st d = p . i holds
p . j = F₃(i,d)
then i + 1 <= len F₁() by FINSEQ_3:25;
then ( 1 <= i & i < len F₁() ) by NAT_1:13, FINSEQ_3:25;
hence for d being DecoratedTree st d = p . i holds
p . j = F₃(i,d) by A3, A1; :: thesis: verum