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 RECDEF_1:sch 5(A1);
take
x
; 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
; ( 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; for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k))
let k be Nat; ( 1 <= k & k < len F1() implies p . (k + 1) = F2((F1() . (k + 1)),(p . k)) )
assume
( 1 <= k & k < len F1() )
; p . (k + 1) = F2((F1() . (k + 1)),(p . k))
hence
p . (k + 1) = F2((F1() . (k + 1)),(p . k))
by A4; verum