defpred S1[ object , object , object ] means for d being DecoratedTree st d = $2 holds
$3 = F3($1,d);
A0: for n being Nat st 1 <= n & n < len F1() holds
for x being set ex y being set st S1[n,x,y]
proof
let n be Nat; :: thesis: ( 1 <= n & n < len F1() implies for x being set ex y being set st S1[n,x,y] )
assume 1 <= n ; :: thesis: ( not n < len F1() or for x being set ex y being set st S1[n,x,y] )
assume n < len F1() ; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
per cases ( x is DecoratedTree or not x is DecoratedTree ) ;
suppose x is DecoratedTree ; :: thesis: ex y being set st S1[n,x,y]
then reconsider xx = x as DecoratedTree ;
take y = F3(n,xx); :: thesis: S1[n,x,y]
thus S1[n,x,y] ; :: thesis: verum
end;
suppose A4: x is not DecoratedTree ; :: thesis: ex y being set st S1[n,x,y]
take y = 0 ; :: thesis: S1[n,x,y]
thus S1[n,x,y] by A4; :: thesis: verum
end;
end;
end;
consider p being FinSequence such that
A1: ( len p = len F1() & ( p . 1 = F2() or len F1() = 0 ) & ( for i being natural set st 1 <= i & i < len F1() holds
S1[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 F1() by A5, A1, FINSEQ_3:29;
defpred S2[ Nat] means ( $1 in dom F1() implies p . $1 is DecoratedTree );
A6: S2[1] by A1;
A7: for i being Nat st i >= 1 & S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( i >= 1 & S2[i] implies S2[i + 1] )
assume A8: ( i >= 1 & S2[i] & i + 1 in dom F1() ) ; :: thesis: p . (i + 1) is DecoratedTree
then AC: i + 1 <= len F1() by FINSEQ_3:25;
then i < len F1() by NAT_1:13;
then reconsider px = p . i as DecoratedTree by A8, FINSEQ_3:25;
p . (i + 1) = F3(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
S2[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 F1() & p . 1 = F2() & ( for i, j being Element of dom F1() st j = i + 1 holds
for d being DecoratedTree st d = p . i holds
p . j = F3(i,d) ) )
thus dom p = dom F1() by A1, FINSEQ_3:29; :: thesis: ( p . 1 = F2() & ( for i, j being Element of dom F1() st j = i + 1 holds
for d being DecoratedTree st d = p . i holds
p . j = F3(i,d) ) )
thus p . 1 = F2() by A1; :: thesis: for i, j being Element of dom F1() st j = i + 1 holds
for d being DecoratedTree st d = p . i holds
p . j = F3(i,d)
let i, j be Element of dom F1(); :: thesis: ( j = i + 1 implies for d being DecoratedTree st d = p . i holds
p . j = F3(i,d) )
assume A3: j = i + 1 ; :: thesis: for d being DecoratedTree st d = p . i holds
p . j = F3(i,d)
then i + 1 <= len F1() by FINSEQ_3:25;
then ( 1 <= i & i < len F1() ) by NAT_1:13, FINSEQ_3:25;
hence for d being DecoratedTree st d = p . i holds
p . j = F3(i,d) by A3, A1; :: thesis: verum