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

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds

f ^ g,n + (len f) is_a_correct_step_wrt X

let n be Nat; :: thesis: for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds

f ^ g,n + (len f) is_a_correct_step_wrt X

let X be Subset of (CQC-WFF Al); :: thesis: for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds

f ^ g,n + (len f) is_a_correct_step_wrt X

let f, g be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( 1 <= n & n <= len g & g,n is_a_correct_step_wrt X implies f ^ g,n + (len f) is_a_correct_step_wrt X )

assume that

A1: 1 <= n and

A2: n <= len g and

A3: g,n is_a_correct_step_wrt X ; :: thesis: f ^ g,n + (len f) is_a_correct_step_wrt X

n in Seg (len g) by A1, A2, FINSEQ_1:1;

then n in dom g by FINSEQ_1:def 3;

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

n + (len f) <= (len f) + (len g) by A2, XREAL_1:6;

then n + (len f) <= len (f ^ g) by FINSEQ_1:22;

then not not ((f ^ g) . (n + (len f))) `2 = 0 & ... & not ((f ^ g) . (n + (len f))) `2 = 9 by A1, Th19, NAT_1:12;

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds

f ^ g,n + (len f) is_a_correct_step_wrt X

let n be Nat; :: thesis: for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds

f ^ g,n + (len f) is_a_correct_step_wrt X

let X be Subset of (CQC-WFF Al); :: thesis: for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds

f ^ g,n + (len f) is_a_correct_step_wrt X

let f, g be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( 1 <= n & n <= len g & g,n is_a_correct_step_wrt X implies f ^ g,n + (len f) is_a_correct_step_wrt X )

assume that

A1: 1 <= n and

A2: n <= len g and

A3: g,n is_a_correct_step_wrt X ; :: thesis: f ^ g,n + (len f) is_a_correct_step_wrt X

n in Seg (len g) by A1, A2, FINSEQ_1:1;

then n in dom g by FINSEQ_1:def 3;

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

n + (len f) <= (len f) + (len g) by A2, XREAL_1:6;

then n + (len f) <= len (f ^ g) by FINSEQ_1:22;

then not not ((f ^ g) . (n + (len f))) `2 = 0 & ... & not ((f ^ g) . (n + (len f))) `2 = 9 by A1, Th19, NAT_1:12;

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

:: according to CQC_THE1:def 4end;

:: according to CQC_THE1:def 4

case
((f ^ g) . (n + (len f))) `2 = 2
; :: thesis: ex p being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (('not' p) => p) => p

hence
ex p being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (('not' p) => p) => p
by A3, A4, Def4; :: thesis: verum

end;case
((f ^ g) . (n + (len f))) `2 = 3
; :: thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = p => (('not' p) => q)

hence
ex p, q being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = p => (('not' p) => q)
by A3, A4, Def4; :: thesis: verum

end;case
((f ^ g) . (n + (len f))) `2 = 4
; :: thesis: ex p, q, r being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))

hence
ex p, q, r being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))
by A3, A4, Def4; :: thesis: verum

end;case
((f ^ g) . (n + (len f))) `2 = 5
; :: thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (p '&' q) => (q '&' p)

hence
ex p, q being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (p '&' q) => (q '&' p)
by A3, A4, Def4; :: thesis: verum

end;case
((f ^ g) . (n + (len f))) `2 = 6
; :: thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ((f ^ g) . (n + (len f))) `1 = (All (x,p)) => p

hence
ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ((f ^ g) . (n + (len f))) `1 = (All (x,p)) => p
by A3, A4, Def4; :: thesis: verum

end;case
((f ^ g) . (n + (len f))) `2 = 7
; :: thesis: ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n + (len f) & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . (n + (len f))) `1 & ((f ^ g) . i) `1 = p => q )

( 1 <= i & i < n + (len f) & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . (n + (len f))) `1 & ((f ^ g) . i) `1 = p => q )

then consider i, j being Nat, r, t being Element of CQC-WFF Al such that

A5: 1 <= i and

A6: i < n and

A7: 1 <= j and

A8: j < i and

A9: ( r = (g . j) `1 & t = (g . n) `1 & (g . i) `1 = r => t ) by A3, A4, Def4;

A10: ( 1 <= i + (len f) & i + (len f) < n + (len f) ) by A5, A6, NAT_1:12, XREAL_1:6;

A11: ( 1 <= j + (len f) & j + (len f) < i + (len f) ) by A7, A8, NAT_1:12, XREAL_1:6;

A12: i <= len g by A2, A6, XXREAL_0:2;

then A13: j <= len g by A8, XXREAL_0:2;

A14: i in Seg (len g) by A5, A12, FINSEQ_1:1;

A15: j in Seg (len g) by A7, A13, FINSEQ_1:1;

A16: i in dom g by A14, FINSEQ_1:def 3;

A17: j in dom g by A15, FINSEQ_1:def 3;

A18: g . i = (f ^ g) . (i + (len f)) by A16, FINSEQ_1:def 7;

g . j = (f ^ g) . (j + (len f)) by A17, FINSEQ_1:def 7;

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

( 1 <= i & i < n + (len f) & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . (n + (len f))) `1 & ((f ^ g) . i) `1 = p => q ) by A4, A9, A10, A11, A18; :: thesis: verum

end;A5: 1 <= i and

A6: i < n and

A7: 1 <= j and

A8: j < i and

A9: ( r = (g . j) `1 & t = (g . n) `1 & (g . i) `1 = r => t ) by A3, A4, Def4;

A10: ( 1 <= i + (len f) & i + (len f) < n + (len f) ) by A5, A6, NAT_1:12, XREAL_1:6;

A11: ( 1 <= j + (len f) & j + (len f) < i + (len f) ) by A7, A8, NAT_1:12, XREAL_1:6;

A12: i <= len g by A2, A6, XXREAL_0:2;

then A13: j <= len g by A8, XXREAL_0:2;

A14: i in Seg (len g) by A5, A12, FINSEQ_1:1;

A15: j in Seg (len g) by A7, A13, FINSEQ_1:1;

A16: i in dom g by A14, FINSEQ_1:def 3;

A17: j in dom g by A15, FINSEQ_1:def 3;

A18: g . i = (f ^ g) . (i + (len f)) by A16, FINSEQ_1:def 7;

g . j = (f ^ g) . (j + (len f)) by A17, FINSEQ_1:def 7;

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

( 1 <= i & i < n + (len f) & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . (n + (len f))) `1 & ((f ^ g) . i) `1 = p => q ) by A4, A9, A10, A11, A18; :: thesis: verum

case
((f ^ g) . (n + (len f))) `2 = 8
; :: thesis: ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n + (len f) & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . (n + (len f))) `1 = p => (All (x,q)) )

( 1 <= i & i < n + (len f) & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . (n + (len f))) `1 = p => (All (x,q)) )

then consider i being Nat, r, t being Element of CQC-WFF Al, x being bound_QC-variable of Al such that

A19: 1 <= i and

A20: i < n and

A21: ( (g . i) `1 = r => t & not x in still_not-bound_in r & (g . n) `1 = r => (All (x,t)) ) by A3, A4, Def4;

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

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

then i in Seg (len g) by A19, FINSEQ_1:1;

then i in dom g by FINSEQ_1:def 3;

then g . i = (f ^ g) . ((len f) + i) by FINSEQ_1:def 7;

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

( 1 <= i & i < n + (len f) & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . (n + (len f))) `1 = p => (All (x,q)) ) by A4, A21, A22; :: thesis: verum

end;A19: 1 <= i and

A20: i < n and

A21: ( (g . i) `1 = r => t & not x in still_not-bound_in r & (g . n) `1 = r => (All (x,t)) ) by A3, A4, Def4;

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

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

then i in Seg (len g) by A19, FINSEQ_1:1;

then i in dom g by FINSEQ_1:def 3;

then g . i = (f ^ g) . ((len f) + i) by FINSEQ_1:def 7;

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

( 1 <= i & i < n + (len f) & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . (n + (len f))) `1 = p => (All (x,q)) ) by A4, A21, A22; :: thesis: verum

case
((f ^ g) . (n + (len f))) `2 = 9
; :: thesis: ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n + (len f) & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . (n + (len f))) `1 )

( 1 <= i & i < n + (len f) & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . (n + (len f))) `1 )

then consider i being Nat, x, y being bound_QC-variable of Al, s being QC-formula of Al such that

A23: 1 <= i and

A24: i < n and

A25: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (g . i) `1 & (g . n) `1 = s . y ) by A3, A4, Def4;

A26: ( 1 <= (len f) + i & (len f) + i < n + (len f) ) by A23, A24, NAT_1:12, XREAL_1:6;

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

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

then i in dom g by FINSEQ_1:def 3;

then g . i = (f ^ g) . ((len f) + i) by FINSEQ_1:def 7;

hence ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n + (len f) & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . (n + (len f))) `1 ) by A4, A25, A26; :: thesis: verum

end;A23: 1 <= i and

A24: i < n and

A25: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (g . i) `1 & (g . n) `1 = s . y ) by A3, A4, Def4;

A26: ( 1 <= (len f) + i & (len f) + i < n + (len f) ) by A23, A24, NAT_1:12, XREAL_1:6;

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

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

then i in dom g by FINSEQ_1:def 3;

then g . i = (f ^ g) . ((len f) + i) by FINSEQ_1:def 7;

hence ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n + (len f) & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . (n + (len f))) `1 ) by A4, A25, A26; :: thesis: verum