defpred S_{1}[ set , set , set ] means $3 = F_{2}($1,$2);

A3: ex p being FinSequence st

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

S_{1}[F_{1}() . (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_{1}() & z = F_{1}() . (k + 1) & S_{1}[z,x,y1] & S_{1}[z,x,y2] holds

y1 = y2 ;

A5: ex p being FinSequence st

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

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

thus F_{3}() = F_{4}()
from RECDEF_1:sch 9(A4, A5, A3); :: thesis: verum

A3: ex p being FinSequence st

( F

S

A4: for k being Nat

for x, y1, y2, z being set st 1 <= k & k < len F

y1 = y2 ;

A5: ex p being FinSequence st

( F

S

thus F