let Al be QC-alphabet ; :: thesis:
let PR, PR1 be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; :: thesis:
let n be Nat; :: thesis:
assume that
A1: 1 <= n and
A2: n <= len PR ; :: thesis:
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:

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

per cases ) . 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 7

case ((PR ^ PR1) . n) `2 = 0 ; :: thesis:

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:

end;

case ((PR ^ PR1) . n) `2 = 1 ; :: thesis:

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

end;

case ((PR ^ PR1) . n) `2 = 2 ; :: thesis:

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:

end;

case ((PR ^ PR1) . n) `2 = 3 ; :: thesis:

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 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 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:

end;

case ((PR ^ PR1) . n) `2 = 4 ; :: thesis:

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 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 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:

end;

case ((PR ^ PR1) . n) `2 = 5 ; :: thesis:

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 = (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 = ((PR ^ PR1) . n) `1 ) by A3, A23, A24, A25, A26, A27, A29; :: thesis:

end;

case ((PR ^ PR1) . n) `2 = 6 ; :: thesis:

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:

end;

case ((PR ^ PR1) . n) `2 = 7 ; :: thesis:

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:

end;

case ((PR ^ PR1) . n) `2 = 8 ; :: thesis:

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:

end;

case ((PR ^ PR1) . n) `2 = 9 ; :: thesis:

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:

end;

assume A42: PR ^ PR1,n is_a_correct_step ; :: thesis:
not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9 by A1, A2, Th31;

per cases ) `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 7

case (PR . n) `2 = 0 ; :: thesis:

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:

end;

case (PR . n) `2 = 1 ; :: thesis:

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

end;

case (PR . n) `2 = 2 ; :: thesis:

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:

end;

case (PR . n) `2 = 3 ; :: thesis:

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 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 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:

end;

case (PR . n) `2 = 4 ; :: thesis:

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 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 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:

end;

case (PR . n) `2 = 5 ; :: thesis:

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 = ((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 = (PR . n) `1 ) by A3, A60, A61, A62, A63, A64, A66; :: thesis:

end;

case (PR . n) `2 = 6 ; :: thesis:

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:

end;

case (PR . n) `2 = 7 ; :: thesis:

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:

end;

case (PR . n) `2 = 8 ; :: thesis:

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:

end;

case (PR . n) `2 = 9 ; :: thesis:

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:

end;