let Al be QC-alphabet ; :: thesis: for n being Nat

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

PR ^ PR1,n + (len PR) is_a_correct_step

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

PR ^ PR1,n + (len PR) is_a_correct_step

let PR, PR1 be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; :: thesis: ( 1 <= n & n <= len PR1 & PR1,n is_a_correct_step implies PR ^ PR1,n + (len PR) is_a_correct_step )

assume that

A1: 1 <= n and

A2: n <= len PR1 and

A3: PR1,n is_a_correct_step ; :: thesis: PR ^ PR1,n + (len PR) is_a_correct_step

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

then A4: PR1 . n = (PR ^ PR1) . (n + (len PR)) by FINSEQ_1:def 7;

n + (len PR) <= (len PR) + (len PR1) by A2, XREAL_1:6;

then A5: n + (len PR) <= len (PR ^ PR1) by FINSEQ_1:22;

not not ((PR ^ PR1) . (n + (len PR))) `2 = 0 & ... & not ((PR ^ PR1) . (n + (len PR))) `2 = 9 by A1, A5, Th31, NAT_1:12;

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

PR ^ PR1,n + (len PR) is_a_correct_step

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

PR ^ PR1,n + (len PR) is_a_correct_step

let PR, PR1 be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; :: thesis: ( 1 <= n & n <= len PR1 & PR1,n is_a_correct_step implies PR ^ PR1,n + (len PR) is_a_correct_step )

assume that

A1: 1 <= n and

A2: n <= len PR1 and

A3: PR1,n is_a_correct_step ; :: thesis: PR ^ PR1,n + (len PR) is_a_correct_step

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

then A4: PR1 . n = (PR ^ PR1) . (n + (len PR)) by FINSEQ_1:def 7;

n + (len PR) <= (len PR) + (len PR1) by A2, XREAL_1:6;

then A5: n + (len PR) <= len (PR ^ PR1) by FINSEQ_1:22;

not not ((PR ^ PR1) . (n + (len PR))) `2 = 0 & ... & not ((PR ^ PR1) . (n + (len PR))) `2 = 9 by A1, A5, Th31, NAT_1:12;

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

:: according to CALCUL_1:def 7end;

:: according to CALCUL_1:def 7

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

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

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

hence
ex f being FinSequence of CQC-WFF Al st

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

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

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

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

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

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

( 1 <= i & i < n + (len PR) & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . (n + (len PR))) `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 & (PR1 . i) `1 = f & (PR1 . n) `1 = g ) by A3, A4, Def7;

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

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

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A6, A7, NAT_1:12, XREAL_1:6;

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

( 1 <= i & i < n + (len PR) & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . (n + (len PR))) `1 = g ) by A4, A8, A9; :: thesis: verum

end;A6: 1 <= i and

A7: i < n and

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

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

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

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A6, A7, NAT_1:12, XREAL_1:6;

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

( 1 <= i & i < n + (len PR) & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . (n + (len PR))) `1 = g ) by A4, A8, A9; :: thesis: verum

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

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `1 )

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `1 )

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

A10: 1 <= i and

A11: i < n and

A12: 1 <= j and

A13: j < i and

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

A15: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A12, A13, NAT_1:12, XREAL_1:6;

A16: i <= len PR1 by A2, A11, XXREAL_0:2;

then i in dom PR1 by A10, FINSEQ_3:25;

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

j <= len PR1 by A13, A16, XXREAL_0:2;

then j in dom PR1 by A12, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A10, A11, NAT_1:12, XREAL_1:6;

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

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `1 ) by A4, A14, A15, A17, A18; :: thesis: verum

end;A10: 1 <= i and

A11: i < n and

A12: 1 <= j and

A13: j < i and

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

A15: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A12, A13, NAT_1:12, XREAL_1:6;

A16: i <= len PR1 by A2, A11, XXREAL_0:2;

then i in dom PR1 by A10, FINSEQ_3:25;

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

j <= len PR1 by A13, A16, XXREAL_0:2;

then j in dom PR1 by A12, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A10, A11, NAT_1:12, XREAL_1:6;

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

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `1 ) by A4, A14, A15, A17, A18; :: thesis: verum

case
((PR ^ PR1) . (n + (len PR))) `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 + (len PR) & 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 + (len PR))) `1 )

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `1 )

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

A19: 1 <= i and

A20: i < n and

A21: 1 <= j and

A22: j < i and

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

A24: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A21, A22, NAT_1:12, XREAL_1:6;

A25: i <= len PR1 by A2, A20, XXREAL_0:2;

then i in dom PR1 by A19, FINSEQ_3:25;

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

j <= len PR1 by A22, A25, XXREAL_0:2;

then j in dom PR1 by A21, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A19, A20, NAT_1:12, XREAL_1:6;

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 + (len PR) & 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 + (len PR))) `1 ) by A4, A23, A24, A26, A27; :: thesis: verum

end;A19: 1 <= i and

A20: i < n and

A21: 1 <= j and

A22: j < i and

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

A24: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A21, A22, NAT_1:12, XREAL_1:6;

A25: i <= len PR1 by A2, A20, XXREAL_0:2;

then i in dom PR1 by A19, FINSEQ_3:25;

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

j <= len PR1 by A22, A25, XXREAL_0:2;

then j in dom PR1 by A21, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A19, A20, NAT_1:12, XREAL_1:6;

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 + (len PR) & 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 + (len PR))) `1 ) by A4, A23, A24, A26, A27; :: thesis: verum

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

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `1 )

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `1 )

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

A28: 1 <= i and

A29: i < n and

A30: 1 <= j and

A31: j < i and

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

A33: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A30, A31, NAT_1:12, XREAL_1:6;

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

then i in dom PR1 by A28, FINSEQ_3:25;

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

j <= len PR1 by A31, A34, XXREAL_0:2;

then j in dom PR1 by A30, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A28, A29, NAT_1:12, XREAL_1:6;

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

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `1 ) by A4, A32, A33, A35, A36; :: thesis: verum

end;A28: 1 <= i and

A29: i < n and

A30: 1 <= j and

A31: j < i and

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

A33: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A30, A31, NAT_1:12, XREAL_1:6;

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

then i in dom PR1 by A28, FINSEQ_3:25;

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

j <= len PR1 by A31, A34, XXREAL_0:2;

then j in dom PR1 by A30, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A28, A29, NAT_1:12, XREAL_1:6;

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

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `1 ) by A4, A32, A33, A35, A36; :: thesis: verum

case
((PR ^ PR1) . (n + (len PR))) `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 + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 )

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

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

A37: 1 <= i and

A38: i < n and

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

i <= len PR1 by A2, A38, XXREAL_0:2;

then i in dom PR1 by A37, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A37, A38, NAT_1:12, XREAL_1:6;

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 + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A39, A40; :: thesis: verum

end;A37: 1 <= i and

A38: i < n and

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

i <= len PR1 by A2, A38, XXREAL_0:2;

then i in dom PR1 by A37, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A37, A38, NAT_1:12, XREAL_1:6;

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 + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A39, A40; :: thesis: verum

case
((PR ^ PR1) . (n + (len PR))) `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 + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . (n + (len PR))) `1 )

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

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

A41: 1 <= i and

A42: i < n and

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

i <= len PR1 by A2, A42, XXREAL_0:2;

then i in dom PR1 by A41, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A41, A42, NAT_1:12, XREAL_1:6;

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 + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A43, A44; :: thesis: verum

end;A41: 1 <= i and

A42: i < n and

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

i <= len PR1 by A2, A42, XXREAL_0:2;

then i in dom PR1 by A41, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A41, A42, NAT_1:12, XREAL_1:6;

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 + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A43, A44; :: thesis: verum

case
((PR ^ PR1) . (n + (len PR))) `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 + (len PR) & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . (n + (len PR))) `1 )

( 1 <= i & i < n + (len PR) & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . (n + (len PR))) `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

A45: 1 <= i and

A46: i < n and

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

i <= len PR1 by A2, A46, XXREAL_0:2;

then i in dom PR1 by A45, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A45, A46, NAT_1:12, XREAL_1:6;

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 + (len PR) & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A47, A48; :: thesis: verum

end;A45: 1 <= i and

A46: i < n and

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

i <= len PR1 by A2, A46, XXREAL_0:2;

then i in dom PR1 by A45, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A45, A46, NAT_1:12, XREAL_1:6;

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 + (len PR) & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A47, A48; :: thesis: verum

case
((PR ^ PR1) . (n + (len PR))) `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 + (len PR) & 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 + (len PR))) `1 )

( 1 <= i & i < n + (len PR) & 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 + (len PR))) `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

A49: 1 <= i and

A50: i < n and

A51: ( 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 = (PR1 . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR1 . n) `1 ) by A3, A4, Def7;

i <= len PR1 by A2, A50, XXREAL_0:2;

then i in dom PR1 by A49, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A49, A50, NAT_1:12, XREAL_1:6;

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 + (len PR) & 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 + (len PR))) `1 ) by A4, A51, A52; :: thesis: verum

end;A49: 1 <= i and

A50: i < n and

A51: ( 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 = (PR1 . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR1 . n) `1 ) by A3, A4, Def7;

i <= len PR1 by A2, A50, XXREAL_0:2;

then i in dom PR1 by A49, FINSEQ_3:25;

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

( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A49, A50, NAT_1:12, XREAL_1:6;

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 + (len PR) & 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 + (len PR))) `1 ) by A4, A51, A52; :: thesis: verum