defpred S_{1}[ 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 S_{1}[n,x,y]

A4: ( len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

S_{1}[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

( 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 S

proof

consider F being FinSequence of CQC-WFF Al such that
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 S_{1}[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 S_{1}[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 S_{1}[n,x,y]

take p => x ; :: thesis: S_{1}[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;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 S

( 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 S

take p => x ; :: thesis: S

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

A4: ( len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

S

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