let n be Element of NAT ; :: thesis:
let X be Subset of CQC-WFF ; :: thesis:
let f, g be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :]; :: thesis:
assume that
A1: 1 <= n and
A2: n <= len f ; :: thesis:
A3: n in Seg (len f) by A1, A2, FINSEQ_1:3;
A4: n in dom f by A3, FINSEQ_1:def 3;
A5: (f ^ g) . n = f . n by A4, FINSEQ_1:def 7;
A6: len (f ^ g) = (len f) + (len g) by FINSEQ_1:35;
A7: len f <= len (f ^ g) by A6, NAT_1:11;
A8: n <= len (f ^ g) by A2, A7, XXREAL_0:2;
thus ( f,n is_a_correct_step_wrt X implies f ^ g,n is_a_correct_step_wrt X ) :: thesis:

assume A9: f,n is_a_correct_step_wrt X ; :: thesis:

per cases ) . n) `2 = 0 or ((f ^ g) . n) `2 = 1 or ((f ^ g) . n) `2 = 2 or ((f ^ g) . n) `2 = 3 or ((f ^ g) . n) `2 = 4 or ((f ^ g) . n) `2 = 5 or ((f ^ g) . n) `2 = 6 or ((f ^ g) . n) `2 = 7 or ((f ^ g) . n) `2 = 8 or ((f ^ g) . n) `2 = 9 ) by A1, A8, Th45;
:: according to CQC_THE1:def 4

case A10: ((f ^ g) . n) `2 = 0 ; :: thesis:

thus ((f ^ g) . n) `1 in X by A5, A9, A10, Def4; :: thesis:

end;

case A11: ((f ^ g) . n) `2 = 1 ; :: thesis:

thus ((f ^ g) . n) `1 = VERUM by A5, A9, A11, Def4; :: thesis:

end;

case A12: ((f ^ g) . n) `2 = 2 ; :: thesis:

thus ex p being Element of CQC-WFF st ((f ^ g) . n) `1 = (('not' p) => p) => p by A5, A9, A12, Def4; :: thesis:

end;

case A13: ((f ^ g) . n) `2 = 3 ; :: thesis:

thus ex p, q being Element of CQC-WFF st ((f ^ g) . n) `1 = p => (('not' p) => q) by A5, A9, A13, Def4; :: thesis:

end;

case A14: ((f ^ g) . n) `2 = 4 ; :: thesis:

thus ex p, q, r being Element of CQC-WFF st ((f ^ g) . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A5, A9, A14, Def4; :: thesis:

end;

case A15: ((f ^ g) . n) `2 = 5 ; :: thesis:

thus ex p, q being Element of CQC-WFF st ((f ^ g) . n) `1 = (p '&' q) => (q '&' p) by A5, A9, A15, Def4; :: thesis:

end;

case A16: ((f ^ g) . n) `2 = 6 ; :: thesis:

thus ex p being Element of CQC-WFF ex x being bound_QC-variable st ((f ^ g) . n) `1 = (All x,p) => p by A5, A9, A16, Def4; :: thesis:

end;

case A17: ((f ^ g) . n) `2 = 7 ; :: thesis:

consider i, j being Element of NAT , r, t being Element of CQC-WFF such that
A18: 1 <= i and
A19: i < n and
A20: 1 <= j and
A21: j < i and
A22: ( r = (f . j) `1 & t = (f . n) `1 & (f . i) `1 = r => t ) by A5, A9, A17, Def4;
A23: i <= len f by A2, A19, XXREAL_0:2;
A24: j <= len f by A21, A23, XXREAL_0:2;
A25: i in Seg (len f) by A18, A23, FINSEQ_1:3;
A26: j in Seg (len f) by A20, A24, FINSEQ_1:3;
A27: i in dom f by A25, FINSEQ_1:def 3;
A28: j in dom f by A26, FINSEQ_1:def 3;
A29: f . i = (f ^ g) . i by A27, FINSEQ_1:def 7;
A30: f . j = (f ^ g) . j by A28, FINSEQ_1:def 7;
thus ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . n) `1 & ((f ^ g) . i) `1 = p => q ) by A5, A18, A19, A20, A21, A22, A29, A30; :: thesis:

end;

case A31: ((f ^ g) . n) `2 = 8 ; :: thesis:

consider i being Element of NAT , r, t being Element of CQC-WFF , x being bound_QC-variable such that
A32: 1 <= i and
A33: i < n and
A34: ( (f . i) `1 = r => t & not x in still_not-bound_in r & (f . n) `1 = r => (All x,t) ) by A5, A9, A31, Def4;
A35: i <= len f by A2, A33, XXREAL_0:2;
A36: i in Seg (len f) by A32, A35, FINSEQ_1:3;
A37: i in dom f by A36, FINSEQ_1:def 3;
A38: f . i = (f ^ g) . i by A37, FINSEQ_1:def 7;
thus ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . n) `1 = p => (All x,q) ) by A5, A32, A33, A34, A38; :: thesis:

end;

case A39: ((f ^ g) . n) `2 = 9 ; :: thesis:

consider i being Element of NAT , x, y being bound_QC-variable, s being QC-formula such that
A40: 1 <= i and
A41: i < n and
A42: ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . n) `1 = s . y ) by A5, A9, A39, Def4;
A43: i <= len f by A2, A41, XXREAL_0:2;
A44: i in Seg (len f) by A40, A43, FINSEQ_1:3;
A45: i in dom f by A44, FINSEQ_1:def 3;
A46: f . i = (f ^ g) . i by A45, FINSEQ_1:def 7;
thus ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . n) `1 ) by A5, A40, A41, A42, A46; :: thesis:

end;

assume A47: f ^ g,n is_a_correct_step_wrt X ; :: thesis:

per cases ) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) by A1, A2, Th45;
:: according to CQC_THE1:def 4

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

thus (f . n) `1 in X by A5, A47, A48, Def4; :: thesis:

end;

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

thus (f . n) `1 = VERUM by A5, A47, A49, Def4; :: thesis:

end;

case A50: (f . n) `2 = 2 ; :: thesis:

thus ex p being Element of CQC-WFF st (f . n) `1 = (('not' p) => p) => p by A5, A47, A50, Def4; :: thesis:

end;

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

thus ex p, q being Element of CQC-WFF st (f . n) `1 = p => (('not' p) => q) by A5, A47, A51, Def4; :: thesis:

end;

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

thus ex p, q, r being Element of CQC-WFF st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A5, A47, A52, Def4; :: thesis:

end;

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

thus ex p, q being Element of CQC-WFF st (f . n) `1 = (p '&' q) => (q '&' p) by A5, A47, A53, Def4; :: thesis:

end;

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

thus ex p being Element of CQC-WFF ex x being bound_QC-variable st (f . n) `1 = (All x,p) => p by A5, A47, A54, Def4; :: thesis:

end;

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

consider i, j being Element of NAT , r, t being Element of CQC-WFF such that
A56: 1 <= i and
A57: i < n and
A58: 1 <= j and
A59: j < i and
A60: ( r = ((f ^ g) . j) `1 & t = ((f ^ g) . n) `1 & ((f ^ g) . i) `1 = r => t ) by A5, A47, A55, Def4;
A61: i <= len f by A2, A57, XXREAL_0:2;
A62: j <= len f by A59, A61, XXREAL_0:2;
A63: i in Seg (len f) by A56, A61, FINSEQ_1:3;
A64: j in Seg (len f) by A58, A62, FINSEQ_1:3;
A65: i in dom f by A63, FINSEQ_1:def 3;
A66: j in dom f by A64, FINSEQ_1:def 3;
A67: f . i = (f ^ g) . i by A65, FINSEQ_1:def 7;
A68: f . j = (f ^ g) . j by A66, FINSEQ_1:def 7;
thus ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A5, A56, A57, A58, A59, A60, A67, A68; :: thesis:

end;

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

consider i being Element of NAT , r, t being Element of CQC-WFF , x being bound_QC-variable such that
A70: 1 <= i and
A71: i < n and
A72: ( ((f ^ g) . i) `1 = r => t & not x in still_not-bound_in r & ((f ^ g) . n) `1 = r => (All x,t) ) by A5, A47, A69, Def4;
A73: i <= len f by A2, A71, XXREAL_0:2;
A74: i in Seg (len f) by A70, A73, FINSEQ_1:3;
A75: i in dom f by A74, FINSEQ_1:def 3;
A76: f . i = (f ^ g) . i by A75, FINSEQ_1:def 7;
thus ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All x,q) ) by A5, A70, A71, A72, A76; :: thesis:

end;

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

consider i being Element of NAT , x, y being bound_QC-variable, s being QC-formula such that
A78: 1 <= i and
A79: i < n and
A80: ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & ((f ^ g) . n) `1 = s . y ) by A5, A47, A77, Def4;
A81: i <= len f by A2, A79, XXREAL_0:2;
A82: i in Seg (len f) by A78, A81, FINSEQ_1:3;
A83: i in dom f by A82, FINSEQ_1:def 3;
A84: f . i = (f ^ g) . i by A83, FINSEQ_1:def 7;
thus ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 ) by A5, A78, A79, A80, A84; :: thesis:

end;