defpred S₁[ object , object , object ] means $3 = F₂($1,$2);
A1: for k being Nat
for x being set st 1 <= k & k < len F₁() holds
ex y being set st S₁[F₁() . (k + 1),x,y] ;
consider x being set such that
A2: ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
S₁[F₁() . (k + 1),p . k,p . (k + 1)] ) ) from RECDEF_1:sch 5(A1);
take x ; :: thesis: ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) )
consider p being FinSequence such that
A3: ( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 ) and
A4: for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) by A2;
take p ; :: thesis: ( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) )
thus ( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 ) by A3; :: thesis: for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k))
let k be Nat; :: thesis: ( 1 <= k & k < len F₁() implies p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) )
assume ( 1 <= k & k < len F₁() ) ; :: thesis: p . (k + 1) = F₂((F₁() . (k + 1)),(p . k))
hence p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) by A4; :: thesis: verum