let Al be QC-alphabet ; :: thesis: for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

for n being Nat st 1 <= n & n <= len PR holds

( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )

let PR, PR1 be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; :: thesis: for n being Nat st 1 <= n & n <= len PR holds

( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )

let n be Nat; :: thesis: ( 1 <= n & n <= len PR implies ( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step ) )

assume that

A1: 1 <= n and

A2: n <= len PR ; :: thesis: ( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )

n in dom PR by A1, A2, FINSEQ_3:25;

then A3: (PR ^ PR1) . n = PR . n by FINSEQ_1:def 7;

len (PR ^ PR1) = (len PR) + (len PR1) by FINSEQ_1:22;

then len PR <= len (PR ^ PR1) by NAT_1:11;

then A4: n <= len (PR ^ PR1) by A2, XXREAL_0:2;

thus ( PR,n is_a_correct_step implies PR ^ PR1,n is_a_correct_step ) :: thesis: ( PR ^ PR1,n is_a_correct_step implies PR,n is_a_correct_step )

not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9 by A1, A2, Th31;

for n being Nat st 1 <= n & n <= len PR holds

( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )

let PR, PR1 be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; :: thesis: for n being Nat st 1 <= n & n <= len PR holds

( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )

let n be Nat; :: thesis: ( 1 <= n & n <= len PR implies ( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step ) )

assume that

A1: 1 <= n and

A2: n <= len PR ; :: thesis: ( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )

n in dom PR by A1, A2, FINSEQ_3:25;

then A3: (PR ^ PR1) . n = PR . n by FINSEQ_1:def 7;

len (PR ^ PR1) = (len PR) + (len PR1) by FINSEQ_1:22;

then len PR <= len (PR ^ PR1) by NAT_1:11;

then A4: n <= len (PR ^ PR1) by A2, XXREAL_0:2;

thus ( PR,n is_a_correct_step implies PR ^ PR1,n is_a_correct_step ) :: thesis: ( PR ^ PR1,n is_a_correct_step implies PR,n is_a_correct_step )

proof

assume A42:
PR ^ PR1,n is_a_correct_step
; :: thesis: PR,n is_a_correct_step
assume A5:
PR,n is_a_correct_step
; :: thesis: PR ^ PR1,n is_a_correct_step

not not ((PR ^ PR1) . n) `2 = 0 & ... & not ((PR ^ PR1) . n) `2 = 9 by A1, A4, Th31;

end;not not ((PR ^ PR1) . n) `2 = 0 & ... & not ((PR ^ PR1) . n) `2 = 9 by A1, A4, Th31;

per cases then
( ((PR ^ PR1) . n) `2 = 0 or ((PR ^ PR1) . n) `2 = 1 or ((PR ^ PR1) . n) `2 = 2 or ((PR ^ PR1) . n) `2 = 3 or ((PR ^ PR1) . n) `2 = 4 or ((PR ^ PR1) . n) `2 = 5 or ((PR ^ PR1) . n) `2 = 6 or ((PR ^ PR1) . n) `2 = 7 or ((PR ^ PR1) . n) `2 = 8 or ((PR ^ PR1) . n) `2 = 9 )
;

:: according to CALCUL_1:def 7end;

:: according to CALCUL_1:def 7

case
((PR ^ PR1) . n) `2 = 0
; :: thesis: ex f being FinSequence of CQC-WFF Al st

( Suc f is_tail_of Ant f & ((PR ^ PR1) . n) `1 = f )

( Suc f is_tail_of Ant f & ((PR ^ PR1) . n) `1 = f )

hence
ex f being FinSequence of CQC-WFF Al st

( Suc f is_tail_of Ant f & ((PR ^ PR1) . n) `1 = f ) by A3, A5, Def7; :: thesis: verum

end;( Suc f is_tail_of Ant f & ((PR ^ PR1) . n) `1 = f ) by A3, A5, Def7; :: thesis: verum

case
((PR ^ PR1) . n) `2 = 1
; :: thesis: ex f being FinSequence of CQC-WFF Al st ((PR ^ PR1) . n) `1 = f ^ <*(VERUM Al)*>

hence
ex f being FinSequence of CQC-WFF Al st ((PR ^ PR1) . n) `1 = f ^ <*(VERUM Al)*>
by A3, A5, Def7; :: thesis: verum

end;case
((PR ^ PR1) . n) `2 = 2
; :: thesis: ex i being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . n) `1 = g )

( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . n) `1 = g )

then consider i being Nat, f, g being FinSequence of CQC-WFF Al such that

A6: 1 <= i and

A7: i < n and

A8: ( Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) by A3, A5, Def7;

i <= len PR by A2, A7, XXREAL_0:2;

then i in dom PR by A6, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . n) `1 = g ) by A3, A6, A7, A8; :: thesis: verum

end;A6: 1 <= i and

A7: i < n and

A8: ( Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) by A3, A5, Def7;

i <= len PR by A2, A7, XXREAL_0:2;

then i in dom PR by A6, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . n) `1 = g ) by A3, A6, A7, A8; :: thesis: verum

case
((PR ^ PR1) . n) `2 = 3
; :: thesis: ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . n) `1 )

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . n) `1 )

then consider i, j being Nat, f, g being FinSequence of CQC-WFF Al such that

A9: 1 <= i and

A10: i < n and

A11: 1 <= j and

A12: j < i and

A13: ( len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) by A3, A5, Def7;

A14: i <= len PR by A2, A10, XXREAL_0:2;

then i in Seg (len PR) by A9, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A15: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A12, A14, XXREAL_0:2;

then j in dom PR by A11, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . n) `1 ) by A3, A9, A10, A11, A12, A13, A15; :: thesis: verum

end;A9: 1 <= i and

A10: i < n and

A11: 1 <= j and

A12: j < i and

A13: ( len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) by A3, A5, Def7;

A14: i <= len PR by A2, A10, XXREAL_0:2;

then i in Seg (len PR) by A9, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A15: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A12, A14, XXREAL_0:2;

then j in dom PR by A11, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . n) `1 ) by A3, A9, A10, A11, A12, A13, A15; :: thesis: verum

case
((PR ^ PR1) . n) `2 = 4
; :: thesis: ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . n) `1 )

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . n) `1 )

then consider i, j being Nat, f, g being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al such that

A16: 1 <= i and

A17: i < n and

A18: 1 <= j and

A19: j < i and

A20: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) by A3, A5, Def7;

A21: i <= len PR by A2, A17, XXREAL_0:2;

then i in Seg (len PR) by A16, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A22: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A19, A21, XXREAL_0:2;

then j in dom PR by A18, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A3, A16, A17, A18, A19, A20, A22; :: thesis: verum

end;A16: 1 <= i and

A17: i < n and

A18: 1 <= j and

A19: j < i and

A20: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) by A3, A5, Def7;

A21: i <= len PR by A2, A17, XXREAL_0:2;

then i in Seg (len PR) by A16, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A22: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A19, A21, XXREAL_0:2;

then j in dom PR by A18, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A3, A16, A17, A18, A19, A20, A22; :: thesis: verum

case
((PR ^ PR1) . n) `2 = 5
; :: thesis: ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . n) `1 )

( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . n) `1 )

then consider i, j being Nat, f, g being FinSequence of CQC-WFF Al such that

A23: 1 <= i and

A24: i < n and

A25: 1 <= j and

A26: j < i and

A27: ( Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) by A3, A5, Def7;

A28: i <= len PR by A2, A24, XXREAL_0:2;

then i in Seg (len PR) by A23, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A29: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A26, A28, XXREAL_0:2;

then j in dom PR by A25, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . n) `1 ) by A3, A23, A24, A25, A26, A27, A29; :: thesis: verum

end;A23: 1 <= i and

A24: i < n and

A25: 1 <= j and

A26: j < i and

A27: ( Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) by A3, A5, Def7;

A28: i <= len PR by A2, A24, XXREAL_0:2;

then i in Seg (len PR) by A23, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A29: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A26, A28, XXREAL_0:2;

then j in dom PR by A25, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . n) `1 ) by A3, A23, A24, A25, A26, A27, A29; :: thesis: verum

case
((PR ^ PR1) . n) `2 = 6
; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 )

( 1 <= i & i < n & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 )

then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that

A30: 1 <= i and

A31: i < n and

A32: ( p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) by A3, A5, Def7;

i <= len PR by A2, A31, XXREAL_0:2;

then i in dom PR by A30, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A3, A30, A31, A32; :: thesis: verum

end;A30: 1 <= i and

A31: i < n and

A32: ( p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) by A3, A5, Def7;

i <= len PR by A2, A31, XXREAL_0:2;

then i in dom PR by A30, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A3, A30, A31, A32; :: thesis: verum

case
((PR ^ PR1) . n) `2 = 7
; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 )

( 1 <= i & i < n & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 )

then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that

A33: 1 <= i and

A34: i < n and

A35: ( p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) by A3, A5, Def7;

i <= len PR by A2, A34, XXREAL_0:2;

then i in dom PR by A33, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 ) by A3, A33, A34, A35; :: thesis: verum

end;A33: 1 <= i and

A34: i < n and

A35: ( p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) by A3, A5, Def7;

i <= len PR by A2, A34, XXREAL_0:2;

then i in dom PR by A33, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 ) by A3, A33, A34, A35; :: thesis: verum

case
((PR ^ PR1) . n) `2 = 8
; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . n) `1 )

( 1 <= i & i < n & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . n) `1 )

then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that

A36: 1 <= i and

A37: i < n and

A38: ( Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) by A3, A5, Def7;

i <= len PR by A2, A37, XXREAL_0:2;

then i in dom PR by A36, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . n) `1 ) by A3, A36, A37, A38; :: thesis: verum

end;A36: 1 <= i and

A37: i < n and

A38: ( Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) by A3, A5, Def7;

i <= len PR by A2, A37, XXREAL_0:2;

then i in dom PR by A36, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . n) `1 ) by A3, A36, A37, A38; :: thesis: verum

case
((PR ^ PR1) . n) `2 = 9
; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All (x,p))*> = ((PR ^ PR1) . n) `1 )

( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All (x,p))*> = ((PR ^ PR1) . n) `1 )

then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that

A39: 1 <= i and

A40: i < n and

A41: ( Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) by A3, A5, Def7;

i <= len PR by A2, A40, XXREAL_0:2;

then i in dom PR by A39, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All (x,p))*> = ((PR ^ PR1) . n) `1 ) by A3, A39, A40, A41; :: thesis: verum

end;A39: 1 <= i and

A40: i < n and

A41: ( Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) by A3, A5, Def7;

i <= len PR by A2, A40, XXREAL_0:2;

then i in dom PR by A39, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All (x,p))*> = ((PR ^ PR1) . n) `1 ) by A3, A39, A40, A41; :: thesis: verum

not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9 by A1, A2, Th31;

per cases then
( (PR . n) `2 = 0 or (PR . n) `2 = 1 or (PR . n) `2 = 2 or (PR . n) `2 = 3 or (PR . n) `2 = 4 or (PR . n) `2 = 5 or (PR . n) `2 = 6 or (PR . n) `2 = 7 or (PR . n) `2 = 8 or (PR . n) `2 = 9 )
;

:: according to CALCUL_1:def 7end;

:: according to CALCUL_1:def 7

case
(PR . n) `2 = 0
; :: thesis: ex f being FinSequence of CQC-WFF Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f )

( Suc f is_tail_of Ant f & (PR . n) `1 = f )

hence
ex f being FinSequence of CQC-WFF Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) by A3, A42, Def7; :: thesis: verum

end;( Suc f is_tail_of Ant f & (PR . n) `1 = f ) by A3, A42, Def7; :: thesis: verum

case
(PR . n) `2 = 1
; :: thesis: ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*>

hence
ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*>
by A3, A42, Def7; :: thesis: verum

end;case
(PR . n) `2 = 2
; :: thesis: ex i being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g )

( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g )

then consider i being Nat, f, g being FinSequence of CQC-WFF Al such that

A43: 1 <= i and

A44: i < n and

A45: ( Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . n) `1 = g ) by A3, A42, Def7;

i <= len PR by A2, A44, XXREAL_0:2;

then i in dom PR by A43, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) by A3, A43, A44, A45; :: thesis: verum

end;A43: 1 <= i and

A44: i < n and

A45: ( Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . n) `1 = g ) by A3, A42, Def7;

i <= len PR by A2, A44, XXREAL_0:2;

then i in dom PR by A43, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) by A3, A43, A44, A45; :: thesis: verum

case
(PR . n) `2 = 3
; :: thesis: ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 )

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 )

then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al such that

A46: 1 <= i and

A47: i < n and

A48: 1 <= j and

A49: j < i and

A50: ( len f > 1 & len f1 > 1 & Ant (Ant f) = Ant (Ant f1) & 'not' (Suc (Ant f)) = Suc (Ant f1) & Suc f = Suc f1 & f = ((PR ^ PR1) . j) `1 & f1 = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

A51: i <= len PR by A2, A47, XXREAL_0:2;

then i in Seg (len PR) by A46, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A52: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A49, A51, XXREAL_0:2;

then j in dom PR by A48, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) by A3, A46, A47, A48, A49, A50, A52; :: thesis: verum

end;A46: 1 <= i and

A47: i < n and

A48: 1 <= j and

A49: j < i and

A50: ( len f > 1 & len f1 > 1 & Ant (Ant f) = Ant (Ant f1) & 'not' (Suc (Ant f)) = Suc (Ant f1) & Suc f = Suc f1 & f = ((PR ^ PR1) . j) `1 & f1 = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

A51: i <= len PR by A2, A47, XXREAL_0:2;

then i in Seg (len PR) by A46, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A52: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A49, A51, XXREAL_0:2;

then j in dom PR by A48, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) by A3, A46, A47, A48, A49, A50, A52; :: thesis: verum

case
(PR . n) `2 = 4
; :: thesis: ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 )

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 )

then consider i, j being Nat, f, g being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al such that

A53: 1 <= i and

A54: i < n and

A55: 1 <= j and

A56: j < i and

A57: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

A58: i <= len PR by A2, A54, XXREAL_0:2;

then i in Seg (len PR) by A53, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A59: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A56, A58, XXREAL_0:2;

then j in dom PR by A55, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) by A3, A53, A54, A55, A56, A57, A59; :: thesis: verum

end;A53: 1 <= i and

A54: i < n and

A55: 1 <= j and

A56: j < i and

A57: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

A58: i <= len PR by A2, A54, XXREAL_0:2;

then i in Seg (len PR) by A53, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A59: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A56, A58, XXREAL_0:2;

then j in dom PR by A55, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) by A3, A53, A54, A55, A56, A57, A59; :: thesis: verum

case
(PR . n) `2 = 5
; :: thesis: ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 )

( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 )

then consider i, j being Nat, f, g being FinSequence of CQC-WFF Al such that

A60: 1 <= i and

A61: i < n and

A62: 1 <= j and

A63: j < i and

A64: ( Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

A65: i <= len PR by A2, A61, XXREAL_0:2;

then i in Seg (len PR) by A60, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A66: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A63, A65, XXREAL_0:2;

then j in dom PR by A62, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) by A3, A60, A61, A62, A63, A64, A66; :: thesis: verum

end;A60: 1 <= i and

A61: i < n and

A62: 1 <= j and

A63: j < i and

A64: ( Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

A65: i <= len PR by A2, A61, XXREAL_0:2;

then i in Seg (len PR) by A60, FINSEQ_1:1;

then i in dom PR by FINSEQ_1:def 3;

then A66: PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

j <= len PR by A63, A65, XXREAL_0:2;

then j in dom PR by A62, FINSEQ_3:25;

then PR . j = (PR ^ PR1) . j by FINSEQ_1:def 7;

hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) by A3, A60, A61, A62, A63, A64, A66; :: thesis: verum

case
(PR . n) `2 = 6
; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 )

( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 )

then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that

A67: 1 <= i and

A68: i < n and

A69: ( p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

i <= len PR by A2, A68, XXREAL_0:2;

then i in dom PR by A67, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) by A3, A67, A68, A69; :: thesis: verum

end;A67: 1 <= i and

A68: i < n and

A69: ( p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

i <= len PR by A2, A68, XXREAL_0:2;

then i in dom PR by A67, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) by A3, A67, A68, A69; :: thesis: verum

case
(PR . n) `2 = 7
; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 )

( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 )

then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that

A70: 1 <= i and

A71: i < n and

A72: ( p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

i <= len PR by A2, A71, XXREAL_0:2;

then i in dom PR by A70, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) by A3, A70, A71, A72; :: thesis: verum

end;A70: 1 <= i and

A71: i < n and

A72: ( p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

i <= len PR by A2, A71, XXREAL_0:2;

then i in dom PR by A70, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) by A3, A70, A71, A72; :: thesis: verum

case
(PR . n) `2 = 8
; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 )

( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 )

then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that

A73: 1 <= i and

A74: i < n and

A75: ( Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

i <= len PR by A2, A74, XXREAL_0:2;

then i in dom PR by A73, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) by A3, A73, A74, A75; :: thesis: verum

end;A73: 1 <= i and

A74: i < n and

A75: ( Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

i <= len PR by A2, A74, XXREAL_0:2;

then i in dom PR by A73, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) by A3, A73, A74, A75; :: thesis: verum

case
(PR . n) `2 = 9
; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 )

( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 )

then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that

A76: 1 <= i and

A77: i < n and

A78: ( Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All (x,p))*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

i <= len PR by A2, A77, XXREAL_0:2;

then i in dom PR by A76, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) by A3, A76, A77, A78; :: thesis: verum

end;A76: 1 <= i and

A77: i < n and

A78: ( Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All (x,p))*> = ((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

i <= len PR by A2, A77, XXREAL_0:2;

then i in dom PR by A76, FINSEQ_3:25;

then PR . i = (PR ^ PR1) . i by FINSEQ_1:def 7;

hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st

( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) by A3, A76, A77, A78; :: thesis: verum