let Al be QC-alphabet ; :: thesis: for n being Nat
for X being Subset of (CQC-WFF Al)
for f, g being FinSequence of st 1 <= n & n <= len f holds
( f,n is_a_correct_step_wrt X iff f ^ g,n 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 st 1 <= n & n <= len f holds
( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

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

let f, g be FinSequence of ; :: thesis: ( 1 <= n & n <= len f implies ( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X ) )
assume that
A1: 1 <= n and
A2: n <= len f ; :: thesis: ( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )
n in Seg (len f) by ;
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 ;
thus ( f,n is_a_correct_step_wrt X implies f ^ g,n is_a_correct_step_wrt X ) :: thesis: ( f ^ g,n is_a_correct_step_wrt X implies f,n is_a_correct_step_wrt X )
proof
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: ((f ^ g) . n) `1 in X
hence ((f ^ g) . n) `1 in X by A3, A5, Def4; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 1 ; :: thesis: ((f ^ g) . n) `1 = VERUM Al
hence ((f ^ g) . n) `1 = VERUM Al by A3, A5, Def4; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 2 ; :: thesis: ex p being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (() => p) => p
hence ex p being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (() => p) => p by A3, A5, Def4; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 3 ; :: thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = p => (() => q)
hence ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = p => (() => q) by A3, A5, Def4; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 4 ; :: thesis: ex p, q, r being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))
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: verum
end;
case ((f ^ g) . n) `2 = 5 ; :: thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p '&' q) => (q '&' p)
hence ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p '&' q) => (q '&' p) by A3, A5, Def4; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 6 ; :: thesis: 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
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: verum
end;
case ((f ^ g) . n) `2 = 7 ; :: thesis: 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 )

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 ;
then A12: j <= len f by ;
A13: i in Seg (len f) by ;
A14: j in Seg (len f) by ;
A15: i in dom f by ;
A16: j in dom f by ;
A17: f . i = (f ^ g) . i by ;
f . j = (f ^ g) . j by ;
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: verum
end;
case ((f ^ g) . n) `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 & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . n) `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
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 ;
then i in Seg (len f) by ;
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: verum
end;
case ((f ^ g) . n) `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 & 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 )

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 ;
then i in Seg (len f) by ;
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: verum
end;
end;
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: (f . n) `1 in X
hence (f . n) `1 in X by ; :: thesis: verum
end;
case (f . n) `2 = 1 ; :: thesis: (f . n) `1 = VERUM Al
hence (f . n) `1 = VERUM Al by ; :: thesis: verum
end;
case (f . n) `2 = 2 ; :: thesis: ex p being Element of CQC-WFF Al st (f . n) `1 = (() => p) => p
hence ex p being Element of CQC-WFF Al st (f . n) `1 = (() => p) => p by ; :: thesis: verum
end;
case (f . n) `2 = 3 ; :: thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (() => q)
hence ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (() => q) by ; :: thesis: verum
end;
case (f . n) `2 = 4 ; :: thesis: ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))
hence ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by ; :: thesis: verum
end;
case (f . n) `2 = 5 ; :: thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p)
hence ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p) by ; :: thesis: verum
end;
case (f . n) `2 = 6 ; :: thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p
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 ; :: thesis: verum
end;
case (f . n) `2 = 7 ; :: thesis: 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 )

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 ;
A30: i <= len f by ;
then A31: j <= len f by ;
A32: i in Seg (len f) by ;
A33: j in Seg (len f) by ;
A34: i in dom f by ;
A35: j in dom f by ;
A36: f . i = (f ^ g) . i by ;
f . j = (f ^ g) . j by ;
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: verum
end;
case (f . n) `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 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `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
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 ;
i <= len f by ;
then i in Seg (len f) by ;
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: verum
end;
case (f . n) `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 & 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 )

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 ;
i <= len f by ;
then i in Seg (len f) by ;
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: verum
end;
end;