let Al be QC-alphabet ; :: thesis: for PR, PR1 being FinSequence of
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 ; :: 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 ;
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 ;
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 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;
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: ex f being FinSequence of CQC-WFF Al st
( 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;
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 )

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 ;
then i in dom PR by ;
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;
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 )

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 ;
then i in Seg (len PR) by ;
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 ;
then j in dom PR by ;
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;
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 )

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 ;
then i in Seg (len PR) by ;
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 ;
then j in dom PR by ;
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;
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 )

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 ;
then i in Seg (len PR) by ;
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 ;
then j in dom PR by ;
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;
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 )

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 ;
then i in dom PR by ;
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;
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 )

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 ;
then i in dom PR by ;
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;
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 )

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 ;
then i in dom PR by ;
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;
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 )

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 ;
then i in dom PR by ;
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;
end;
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: ex f being FinSequence of CQC-WFF Al st
( 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 ; :: thesis: verum
end;
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 ; :: 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 )

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 ;
i <= len PR by ;
then i in dom PR by ;
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;
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 )

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 ;
A51: i <= len PR by ;
then i in Seg (len PR) by ;
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 ;
then j in dom PR by ;
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;
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 )

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 ;
A58: i <= len PR by ;
then i in Seg (len PR) by ;
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 ;
then j in dom PR by ;
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;
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 )

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 ;
A65: i <= len PR by ;
then i in Seg (len PR) by ;
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 ;
then j in dom PR by ;
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;
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 )

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 ;
i <= len PR by ;
then i in dom PR by ;
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;
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 )

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 ;
i <= len PR by ;
then i in dom PR by ;
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;
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 )

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 ;
i <= len PR by ;
then i in dom PR by ;
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;
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 )

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 ;
i <= len PR by ;
then i in dom PR by ;
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;
end;