let Al be QC-alphabet ; :: thesis:
let n be Nat; :: thesis:
let X be Subset of (CQC-WFF Al); :: thesis:
let f, g be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis:
assume that
A1: 1 <= n and
A2: n <= len f ; :: thesis:
n in Seg (len f) by A1, A2, FINSEQ_1:1;
then n in dom f by FINSEQ_1:def 3;
then A3: (f ^ g) . n = f . n by FINSEQ_1:def 7;
len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then len f <= len (f ^ g) by NAT_1:11;
then A4: n <= len (f ^ g) by A2, XXREAL_0:2;
thus ( f,n is_a_correct_step_wrt X implies f ^ g,n is_a_correct_step_wrt X ) :: thesis:

assume A5: f,n is_a_correct_step_wrt X ; :: thesis:
not not ((f ^ g) . n) `2 = 0 & ... & not ((f ^ g) . n) `2 = 9 by A1, A4, Th19;

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 ) ;
:: according to CQC_THE1:def 4

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

hence ((f ^ g) . n) `1 in X by A3, A5, Def4; :: thesis:

end;

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

hence ((f ^ g) . n) `1 = VERUM Al by A3, A5, Def4; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

then consider i, j being Nat, r, t being Element of CQC-WFF Al such that
A6: 1 <= i and
A7: i < n and
A8: 1 <= j and
A9: j < i and
A10: ( r = (f . j) `1 & t = (f . n) `1 & (f . i) `1 = r => t ) by A3, A5, Def4;
A11: i <= len f by A2, A7, XXREAL_0:2;
then A12: j <= len f by A9, XXREAL_0:2;
A13: i in Seg (len f) by A6, A11, FINSEQ_1:1;
A14: j in Seg (len f) by A8, A12, FINSEQ_1:1;
A15: i in dom f by A13, FINSEQ_1:def 3;
A16: j in dom f by A14, FINSEQ_1:def 3;
A17: f . i = (f ^ g) . i by A15, FINSEQ_1:def 7;
f . j = (f ^ g) . j by A16, FINSEQ_1:def 7;
hence ex i, j being Nat ex p, q being Element of CQC-WFF Al 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 A3, A6, A7, A8, A9, A10, A17; :: thesis:

end;

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

then consider i being Nat, r, t being Element of CQC-WFF Al, x being bound_QC-variable of Al such that
A18: 1 <= i and
A19: i < n and
A20: ( (f . i) `1 = r => t & not x in still_not-bound_in r & (f . n) `1 = r => (All (x,t)) ) by A3, A5, Def4;
i <= len f by A2, A19, XXREAL_0:2;
then i in Seg (len f) by A18, FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then f . i = (f ^ g) . 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 & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . n) `1 = p => (All (x,q)) ) by A3, A18, A19, A20; :: thesis:

end;

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

then consider i being Nat, x, y being bound_QC-variable of Al, s being QC-formula of Al such that
A21: 1 <= i and
A22: i < n and
A23: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . n) `1 = s . y ) by A3, A5, Def4;
i <= len f by A2, A22, XXREAL_0:2;
then i in Seg (len f) by A21, FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then f . i = (f ^ g) . 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 & 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) `1 ) by A3, A21, A22, A23; :: thesis:

end;

assume A24: f ^ g,n is_a_correct_step_wrt X ; :: thesis:
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9 by A1, A2, Th19;

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 ) ;
:: according to CQC_THE1:def 4

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

hence (f . n) `1 in X by A3, A24, Def4; :: thesis:

end;

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

hence (f . n) `1 = VERUM Al by A3, A24, Def4; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

then consider i, j being Nat, r, t being Element of CQC-WFF Al such that
A25: 1 <= i and
A26: i < n and
A27: 1 <= j and
A28: j < i and
A29: ( r = ((f ^ g) . j) `1 & t = ((f ^ g) . n) `1 & ((f ^ g) . i) `1 = r => t ) by A3, A24, Def4;
A30: i <= len f by A2, A26, XXREAL_0:2;
then A31: j <= len f by A28, XXREAL_0:2;
A32: i in Seg (len f) by A25, A30, FINSEQ_1:1;
A33: j in Seg (len f) by A27, A31, FINSEQ_1:1;
A34: i in dom f by A32, FINSEQ_1:def 3;
A35: j in dom f by A33, FINSEQ_1:def 3;
A36: f . i = (f ^ g) . i by A34, FINSEQ_1:def 7;
f . j = (f ^ g) . j by A35, FINSEQ_1:def 7;
hence ex i, j being Nat ex p, q being Element of CQC-WFF Al st
( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A3, A25, A26, A27, A28, A29, A36; :: thesis:

end;

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

then consider i being Nat, r, t being Element of CQC-WFF Al, x being bound_QC-variable of Al such that
A37: 1 <= i and
A38: i < n and
A39: ( ((f ^ g) . i) `1 = r => t & not x in still_not-bound_in r & ((f ^ g) . n) `1 = r => (All (x,t)) ) by A3, A24, Def4;
i <= len f by A2, A38, XXREAL_0:2;
then i in Seg (len f) by A37, FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then f . i = (f ^ g) . 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 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) by A3, A37, A38, A39; :: thesis:

end;

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

then consider i being Nat, x, y being bound_QC-variable of Al, s being QC-formula of Al such that
A40: 1 <= i and
A41: i < n and
A42: ( 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 & ((f ^ g) . n) `1 = s . y ) by A3, A24, Def4;
i <= len f by A2, A41, XXREAL_0:2;
then i in Seg (len f) by A40, FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then f . i = (f ^ g) . 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 & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 ) by A3, A40, A41, A42; :: thesis:

end;