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