let n be Element of NAT ; :: thesis: for X being Subset of CQC-WFF
for g, f being FinSequence of [:CQC-WFF,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; :: thesis: for g, f being FinSequence of [:CQC-WFF,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 g, f be FinSequence of [:CQC-WFF,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 A5: n + (len f) <= len (f ^ g) by FINSEQ_1:22;

per cases ( ((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 ) by A1, A5, Th45, NAT_1:12;
:: according to CQC_THE1:def 4

case ((f ^ g) . (n + (len f))) `2 = 0 ; :: thesis: ((f ^ g) . (n + (len f))) `1 in X

hence ((f ^ g) . (n + (len f))) `1 in X by A3, A4, Def4; :: thesis: verum

end;

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

hence ((f ^ g) . (n + (len f))) `1 = VERUM by A3, A4, Def4; :: thesis: verum

end;

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

hence ex p being Element of CQC-WFF 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 st ((f ^ g) . (n + (len f))) `1 = p => (('not' p) => q)

hence ex p, q being Element of CQC-WFF 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 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 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 st ((f ^ g) . (n + (len f))) `1 = (p '&' q) => (q '&' p)

hence ex p, q being Element of CQC-WFF 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 ex x being bound_QC-variable st ((f ^ g) . (n + (len f))) `1 = (All (x,p)) => p

hence ex p being Element of CQC-WFF ex x being bound_QC-variable 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 Element of NAT ex p, q being Element of CQC-WFF 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 )

then consider i, j being Element of NAT , r, t being Element of CQC-WFF such that
A6: 1 <= i and
A7: i < n and
A8: 1 <= j and
A9: j < i and
A10: ( r = (g . j) `1 & t = (g . n) `1 & (g . i) `1 = r => t ) by A3, A4, Def4;
A11: ( 1 <= i + (len f) & i + (len f) < n + (len f) ) by A6, A7, NAT_1:12, XREAL_1:6;
A12: ( 1 <= j + (len f) & j + (len f) < i + (len f) ) by A8, A9, NAT_1:12, XREAL_1:6;
A13: i <= len g by A2, A7, XXREAL_0:2;
then A14: j <= len g by A9, XXREAL_0:2;
A15: i in Seg (len g) by A6, A13, FINSEQ_1:1;
A16: j in Seg (len g) by A8, A14, FINSEQ_1:1;
A17: i in dom g by A15, FINSEQ_1:def 3;
A18: j in dom g by A16, FINSEQ_1:def 3;
A19: g . i = (f ^ g) . (i + (len f)) by A17, FINSEQ_1:def 7;
g . j = (f ^ g) . (j + (len f)) by A18, 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 + (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, A10, A11, A12, A19; :: thesis: verum

end;

case ((f ^ g) . (n + (len f))) `2 = 8 ; :: thesis: 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 + (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 Element of NAT , r, t being Element of CQC-WFF , x being bound_QC-variable such that
A20: 1 <= i and
A21: i < n and
A22: ( (g . i) `1 = r => t & not x in still_not-bound_in r & (g . n) `1 = r => (All (x,t)) ) by A3, A4, Def4;
A23: ( 1 <= (len f) + i & (len f) + i < n + (len f) ) by A20, A21, NAT_1:12, XREAL_1:6;
i <= len g by A2, A21, XXREAL_0:2;
then i in Seg (len g) by A20, 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 Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable 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, A22, A23; :: thesis: verum

end;

case ((f ^ g) . (n + (len f))) `2 = 9 ; :: thesis: ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n + (len f) & 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 + (len f))) `1 )

then consider i being Element of NAT , x, y being bound_QC-variable, s being QC-formula such that
A24: 1 <= i and
A25: i < n and
A26: ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (g . i) `1 & (g . n) `1 = s . y ) by A3, A4, Def4;
A27: ( 1 <= (len f) + i & (len f) + i < n + (len f) ) by A24, A25, NAT_1:12, XREAL_1:6;
i <= len g by A2, A25, XXREAL_0:2;
then i in Seg (len g) by A24, 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 Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n + (len f) & 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 + (len f))) `1 ) by A4, A26, A27; :: thesis: verum

end;

end;