defpred S1[ set , set , set ] means $3 = F2($1,$2);
A1:
for k being Element of 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
A3:
ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of 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
; :: thesis: ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
consider p being FinSequence such that
A4:
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
by A3;
take
p
; :: thesis: ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of 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 A4; :: thesis: for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k))
let k be Element of 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