defpred S1[ object , object , object ] means \$3 = F2(\$1,\$2);
A1: for k being Nat
for x being set st 1 <= k & k < len F1() holds
ex y being set st S1[F1() . (k + 1),x,y] ;
consider x being set such that
A2: ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
S1[F1() . (k + 1),p . k,p . (k + 1)] ) ) from take x ; :: thesis: ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )

consider p being FinSequence such that
A3: ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 ) and
A4: for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) by A2;
take p ; :: thesis: ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )

thus ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 ) by A3; :: thesis: for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k))

let k be Nat; :: thesis: ( 1 <= k & k < len F1() implies p . (k + 1) = F2((F1() . (k + 1)),(p . k)) )
assume ( 1 <= k & k < len F1() ) ; :: thesis: p . (k + 1) = F2((F1() . (k + 1)),(p . k))
hence p . (k + 1) = F2((F1() . (k + 1)),(p . k)) by A4; :: thesis: verum