defpred S1[ object , object , object ] means $3 = F3($1,$2);
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]
;
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;
take
p
; ( dom p = dom F1() & p . 1 = F2() & ( for i, j being Element of dom F1() st j = i + 1 holds
p . j = F3(i,(p . i)) ) )
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
p . j = F3(i,(p . i)) ) )
thus
p . 1 = F2()
by A1; for i, j being Element of dom F1() st j = i + 1 holds
p . j = F3(i,(p . i))
let i, j be Element of dom F1(); ( j = i + 1 implies p . j = F3(i,(p . i)) )
assume A3:
j = i + 1
; p . j = F3(i,(p . i))
then
i + 1 <= len F1()
by FINSEQ_3:25;
then
( 1 <= i & i < len F1() )
by NAT_1:13, FINSEQ_3:25;
hence
p . j = F3(i,(p . i))
by A3, A1; verum