defpred S₁[ 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₁[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₁[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₁[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₁[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₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
G = H from RECDEF_1:sch 8(A11, A10, A8);
hence p1 = p2 by A9, A7; :: thesis: verum