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