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 A1: ( 1 <= n & n <= len f ) ; :: thesis:
then n in Seg (len f) by FINSEQ_1:3;
then n in dom f by FINSEQ_1:def 3;
then A2: (f ^ g) . n = f . n by FINSEQ_1:def 7;
len (f ^ g) = (len f) + (len g) by FINSEQ_1:35;
then len f <= len (f ^ g) by NAT_1:11;
then A3: ( 1 <= n & n <= len (f ^ g) ) by A1, XXREAL_0:2;
thus ( f,n is_a_correct_step_wrt X implies f ^ g,n is_a_correct_step_wrt X ) :: thesis:

proof

assume A4: 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 A3, Th45;
:: according to CQC_THE1:def 4

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

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

end;

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

hence ((f ^ g) . n) `1 = VERUM by A2, A4, Def4; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

then consider i, j being Element of NAT , r, t being Element of CQC-WFF such that
A5: ( 1 <= i & i < n & 1 <= j & j < i ) and
A6: r = (f . j) `1 and
A7: t = (f . n) `1 and
A8: (f . i) `1 = r => t by A2, A4, Def4;
( i <= len f & j <= n ) by A1, A5, XXREAL_0:2;
then ( i in Seg (len f) & j <= len f ) by A5, FINSEQ_1:3, XXREAL_0:2;
then ( i in Seg (len f) & j in Seg (len f) ) by A5, FINSEQ_1:3;
then ( i in dom f & j in dom f ) by FINSEQ_1:def 3;
then ( f . i = (f ^ g) . i & f . j = (f ^ g) . j ) by FINSEQ_1:def 7;
hence 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 A2, A5, A6, A7, A8; :: thesis:

end;

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

then consider i being Element of NAT , r, t being Element of CQC-WFF , x being bound_QC-variable such that
A9: ( 1 <= i & i < n ) and
A10: ( (f . i) `1 = r => t & not x in still_not-bound_in r & (f . n) `1 = r => (All x,t) ) by A2, A4, Def4;
i <= len f by A1, A9, XXREAL_0:2;
then i in Seg (len f) by A9, FINSEQ_1:3;
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 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 A2, A9, A10; :: thesis:

end;

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

then consider i being Element of NAT , x, y being bound_QC-variable, s being QC-formula such that
A11: ( 1 <= i & i < n ) and
A12: ( 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 A2, A4, Def4;
i <= len f by A1, A11, XXREAL_0:2;
then i in Seg (len f) by A11, FINSEQ_1:3;
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 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 A2, A11, A12; :: thesis:

end;

assume A13: 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, Th45;
:: according to CQC_THE1:def 4

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

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

end;

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

hence (f . n) `1 = VERUM by A2, A13, Def4; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

then consider i, j being Element of NAT , r, t being Element of CQC-WFF such that
A14: ( 1 <= i & i < n & 1 <= j & j < i ) and
A15: r = ((f ^ g) . j) `1 and
A16: t = ((f ^ g) . n) `1 and
A17: ((f ^ g) . i) `1 = r => t by A2, A13, Def4;
( i <= len f & j <= n ) by A1, A14, XXREAL_0:2;
then ( i in Seg (len f) & j <= len f ) by A14, FINSEQ_1:3, XXREAL_0:2;
then ( i in Seg (len f) & j in Seg (len f) ) by A14, FINSEQ_1:3;
then ( i in dom f & j in dom f ) by FINSEQ_1:def 3;
then ( f . i = (f ^ g) . i & f . j = (f ^ g) . j ) by FINSEQ_1:def 7;
hence 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 A2, A14, A15, A16, A17; :: thesis:

end;

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

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

end;

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

then consider i being Element of NAT , x, y being bound_QC-variable, s being QC-formula such that
A20: ( 1 <= i & i < n ) and
A21: ( 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 A2, A13, Def4;
i <= len f by A1, A20, XXREAL_0:2;
then i in Seg (len f) by A20, FINSEQ_1:3;
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 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 A2, A20, A21; :: thesis:

end;