defpred S₁[ set , set , set ] means $3 = F₂($1,$2);
A3: ex p being FinSequence st
( F₄() = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
S₁[F₁() . (k + 1),p . k,p . (k + 1)] ) ) by A2;
A4: for k being Nat
for x, y1, y2, z being set st 1 <= k & k < len F₁() & z = F₁() . (k + 1) & S₁[z,x,y1] & S₁[z,x,y2] holds
y1 = y2 ;
A5: ex p being FinSequence st
( F₃() = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
S₁[F₁() . (k + 1),p . k,p . (k + 1)] ) ) by A1;
thus F₃() = F₄() from RECDEF_1:sch 9(A4, A5, A3); :: thesis: verum