defpred S1[ Element of NAT , set , set ] means ex p, q being Element of CQC-WFF st
( p = f . ($1 + 1) & q = $2 & $3 = p => q );
A2:
for n being Element of NAT st 1 <= n & n < len f holds
for x being Element of CQC-WFF ex y being Element of CQC-WFF st S1[n,x,y]
proof
let n be
Element of
NAT ;
:: thesis: ( 1 <= n & n < len f implies for x being Element of CQC-WFF ex y being Element of CQC-WFF st S1[n,x,y] )
assume A3:
( 1
<= n &
n < len f )
;
:: thesis: for x being Element of CQC-WFF ex y being Element of CQC-WFF st S1[n,x,y]
let x be
Element of
CQC-WFF ;
:: thesis: ex y being Element of CQC-WFF st S1[n,x,y]
A4:
1
<= n + 1
by NAT_1:11;
n + 1
<= len f
by A3, NAT_1:13;
then
n + 1
in dom f
by A4, FINSEQ_3:27;
then reconsider p =
f . (n + 1) as
Element of
CQC-WFF by FINSEQ_2:13;
take y =
p => x;
:: thesis: S1[n,x,y]
take
p
;
:: thesis: ex q being Element of CQC-WFF st
( p = f . (n + 1) & q = x & y = p => q )
take
x
;
:: thesis: ( p = f . (n + 1) & x = x & y = p => x )
thus
(
p = f . (n + 1) &
x = x &
y = p => x )
;
:: thesis: verum
end;
consider F being FinSequence of CQC-WFF such that
A5:
( len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
S1[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 4(A2);
len f in dom F
by A1, A5, FINSEQ_3:27;
then reconsider p = F . (len f) as Element of CQC-WFF by FINSEQ_2:13;
take
p
; :: thesis: ex F being FinSequence of CQC-WFF st
( p = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) )
thus
ex F being FinSequence of CQC-WFF st
( p = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) )
by A5; :: thesis: verum