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 );

let p1, p2 be Element of CQC-WFF Al; :: thesis: ( ex F being FinSequence of CQC-WFF Al st

( p1 = 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 ) ) ) & ex F being FinSequence of CQC-WFF Al st

( p2 = 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 ) ) ) implies p1 = p2 )

assume that

A5: ex F being FinSequence of CQC-WFF Al st

( p1 = 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

S_{1}[n,F . n,F . (n + 1)] ) )
and

A6: ex F being FinSequence of CQC-WFF Al st

( p2 = 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

S_{1}[n,F . n,F . (n + 1)] ) )
; :: thesis: p1 = p2

consider H being FinSequence of CQC-WFF Al such that

A7: p2 = H . (len f) and

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

S_{1}[n,H . n,H . (n + 1)] ) )
by A6;

consider G being FinSequence of CQC-WFF Al such that

A9: p1 = G . (len f) and

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

S_{1}[n,G . n,G . (n + 1)] ) )
by A5;

A11: for n being Nat st 1 <= n & n < len f holds

for x, y1, y2 being Element of CQC-WFF Al st S_{1}[n,x,y1] & S_{1}[n,x,y2] holds

y1 = y2 ;

G = H from RECDEF_1:sch 8(A11, A10, A8);

hence p1 = p2 by A9, A7; :: thesis: verum

( p = f . ($1 + 1) & q = $2 & $3 = p => q );

let p1, p2 be Element of CQC-WFF Al; :: thesis: ( ex F being FinSequence of CQC-WFF Al st

( p1 = 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 ) ) ) & ex F being FinSequence of CQC-WFF Al st

( p2 = 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 ) ) ) implies p1 = p2 )

assume that

A5: ex F being FinSequence of CQC-WFF Al st

( p1 = 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

S

A6: ex F being FinSequence of CQC-WFF Al st

( p2 = 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

S

consider H being FinSequence of CQC-WFF Al such that

A7: p2 = H . (len f) and

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

S

consider G being FinSequence of CQC-WFF Al such that

A9: p1 = G . (len f) and

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

S

A11: for n being Nat st 1 <= n & n < len f holds

for x, y1, y2 being Element of CQC-WFF Al st S

y1 = y2 ;

G = H from RECDEF_1:sch 8(A11, A10, A8);

hence p1 = p2 by A9, A7; :: thesis: verum