defpred S_{1}[ Nat, set , set ] means P_{1}[F_{1}() . ($1 + 1),$2,$3];

A4: for k being Nat st 1 <= k & k < len F_{1}() holds

for x, y1, y2 being set st S_{1}[k,x,y1] & S_{1}[k,x,y2] holds

y1 = y2 by A1;

consider q being FinSequence such that

A5: F_{3}() = q . (len q)
and

A6: ( len q = len F_{1}() & q . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

S_{1}[k,q . k,q . (k + 1)] ) )
by A3;

A7: ( len q = len F_{1}() & ( q . 1 = F_{1}() . 1 or len F_{1}() = 0 ) & ( for k being Nat st 1 <= k & k < len F_{1}() holds

S_{1}[k,q . k,q . (k + 1)] ) )
by A6;

consider p being FinSequence such that

A8: F_{2}() = p . (len p)
and

A9: ( len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

S_{1}[k,p . k,p . (k + 1)] ) )
by A2;

A10: ( len p = len F_{1}() & ( p . 1 = F_{1}() . 1 or len F_{1}() = 0 ) & ( for k being Nat st 1 <= k & k < len F_{1}() holds

S_{1}[k,p . k,p . (k + 1)] ) )
by A9;

p = q from RECDEF_1:sch 7(A4, A10, A7);

hence F_{2}() = F_{3}()
by A8, A5; :: thesis: verum

A4: for k being Nat st 1 <= k & k < len F

for x, y1, y2 being set st S

y1 = y2 by A1;

consider q being FinSequence such that

A5: F

A6: ( len q = len F

S

A7: ( len q = len F

S

consider p being FinSequence such that

A8: F

A9: ( len p = len F

S

A10: ( len p = len F

S

p = q from RECDEF_1:sch 7(A4, A10, A7);

hence F