defpred S₁[ Nat, set , set ] means P₁[F₁() . ($1 + 1),$2,$3];
A4: for k being Nat st 1 <= k & k < len F₁() holds
for x, y1, y2 being set st S₁[k,x,y1] & S₁[k,x,y2] holds
y1 = y2 by A1;
consider q being FinSequence such that
A5: F₃() = q . (len q) and
A6: ( len q = len F₁() & q . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
S₁[k,q . k,q . (k + 1)] ) ) by A3;
A7: ( len q = len F₁() & ( q . 1 = F₁() . 1 or len F₁() = 0 ) & ( for k being Nat st 1 <= k & k < len F₁() holds
S₁[k,q . k,q . (k + 1)] ) ) by A6;
consider p being FinSequence such that
A8: F₂() = p . (len p) and
A9: ( len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
S₁[k,p . k,p . (k + 1)] ) ) by A2;
A10: ( len p = len F₁() & ( p . 1 = F₁() . 1 or len F₁() = 0 ) & ( for k being Nat st 1 <= k & k < len F₁() holds
S₁[k,p . k,p . (k + 1)] ) ) by A9;
p = q from RECDEF_1:sch 7(A4, A10, A7);
hence F₂() = F₃() by A8, A5; :: thesis: verum