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;
( 1 <= n & n < len F1() implies for x being set ex y being set st S1[n,x,y] )
assume
1
<= n
;
( not n < len F1() or for x being set ex y being set st S1[n,x,y] )
assume
n < len F1()
;
for x being set ex y being set st S1[n,x,y]
let x be
set ;
ex y being set st S1[n,x,y]
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
then reconsider p = p as non empty DTree-yielding FinSequence ;
take
p
; ( 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; ( 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; 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(); ( j = i + 1 implies for d being DecoratedTree st d = p . i holds
p . j = F3(i,d) )
assume A3:
j = i + 1
; 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; verum