let n be Element of NAT ; :: thesis: for PR1, PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st 1 <= n & n <= len PR1 & PR1,n is_a_correct_step holds
PR ^ PR1,n + (len PR) is_a_correct_step
let PR1, PR be FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :]; :: thesis: ( 1 <= n & n <= len PR1 & PR1,n is_a_correct_step implies PR ^ PR1,n + (len PR) is_a_correct_step )
assume that
A1: ( 1 <= n & n <= len PR1 ) and
A2: PR1,n is_a_correct_step ; :: thesis: PR ^ PR1,n + (len PR) is_a_correct_step
n in dom PR1 by A1, FINSEQ_3:27;
then A3: PR1 . n = (PR ^ PR1) . (n + (len PR)) by FINSEQ_1:def 7;
n + (len PR) <= (len PR) + (len PR1) by A1, XREAL_1:8;
then A4: ( 1 <= n + (len PR) & n + (len PR) <= len (PR ^ PR1) ) by A1, FINSEQ_1:35, NAT_1:12;

per cases ( ((PR ^ PR1) . (n + (len PR))) `2 = 0 or ((PR ^ PR1) . (n + (len PR))) `2 = 1 or ((PR ^ PR1) . (n + (len PR))) `2 = 2 or ((PR ^ PR1) . (n + (len PR))) `2 = 3 or ((PR ^ PR1) . (n + (len PR))) `2 = 4 or ((PR ^ PR1) . (n + (len PR))) `2 = 5 or ((PR ^ PR1) . (n + (len PR))) `2 = 6 or ((PR ^ PR1) . (n + (len PR))) `2 = 7 or ((PR ^ PR1) . (n + (len PR))) `2 = 8 or ((PR ^ PR1) . (n + (len PR))) `2 = 9 ) by A4, Th31;
:: according to CALCUL_1:def 7

case ((PR ^ PR1) . (n + (len PR))) `2 = 0 ; :: thesis: ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & ((PR ^ PR1) . (n + (len PR))) `1 = f )

hence ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & ((PR ^ PR1) . (n + (len PR))) `1 = f ) by A2, A3, Def7; :: thesis: verum

end;

case ((PR ^ PR1) . (n + (len PR))) `2 = 1 ; :: thesis: ex f being FinSequence of CQC-WFF st ((PR ^ PR1) . (n + (len PR))) `1 = f ^ <*VERUM *>

hence ex f being FinSequence of CQC-WFF st ((PR ^ PR1) . (n + (len PR))) `1 = f ^ <*VERUM *> by A2, A3, Def7; :: thesis: verum

end;

case ((PR ^ PR1) . (n + (len PR))) `2 = 2 ; :: thesis: ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n + (len PR) & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . (n + (len PR))) `1 = g )

then consider i being Element of NAT , f, g being FinSequence of CQC-WFF such that
A5: ( 1 <= i & i < n ) and
A6: ( Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR1 . i) `1 = f & (PR1 . n) `1 = g ) by A2, A3, Def7;
A7: ( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A5, NAT_1:12, XREAL_1:8;
i <= len PR1 by A1, A5, XXREAL_0:2;
then i in dom PR1 by A5, FINSEQ_3:27;
then PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
hence ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n + (len PR) & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . (n + (len PR))) `1 = g ) by A3, A6, A7; :: thesis: verum

end;

case ((PR ^ PR1) . (n + (len PR))) `2 = 3 ; :: thesis: ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . (n + (len PR))) `1 )

then consider i, j being Element of NAT , f, f1 being FinSequence of CQC-WFF such that
A8: ( 1 <= i & i < n & 1 <= j & j < i ) and
A9: ( len f > 1 & len f1 > 1 & Ant (Ant f) = Ant (Ant f1) & 'not' (Suc (Ant f)) = Suc (Ant f1) & Suc f = Suc f1 & f = (PR1 . j) `1 & f1 = (PR1 . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR1 . n) `1 ) by A2, A3, Def7;
A10: ( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A8, NAT_1:12, XREAL_1:8;
A11: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A8, NAT_1:12, XREAL_1:8;
A12: ( i <= len PR1 & j <= n ) by A1, A8, XXREAL_0:2;
then ( i in Seg (len PR1) & j <= len PR1 ) by A8, FINSEQ_1:3, XXREAL_0:2;
then ( i in dom PR1 & j in dom PR1 ) by A8, A12, FINSEQ_3:27;
then ( PR1 . i = (PR ^ PR1) . ((len PR) + i) & PR1 . j = (PR ^ PR1) . ((len PR) + j) ) by FINSEQ_1:def 7;
hence ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A3, A9, A10, A11; :: thesis: verum

end;

case ((PR ^ PR1) . (n + (len PR))) `2 = 4 ; :: thesis: ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 )

then consider i, j being Element of NAT , f, g being FinSequence of CQC-WFF , p being Element of CQC-WFF such that
A13: ( 1 <= i & i < n & 1 <= j & j < i ) and
A14: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR1 . j) `1 & g = (PR1 . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR1 . n) `1 ) by A2, A3, Def7;
A15: ( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A13, NAT_1:12, XREAL_1:8;
A16: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A13, NAT_1:12, XREAL_1:8;
A17: ( i <= len PR1 & j <= n ) by A1, A13, XXREAL_0:2;
then ( i in Seg (len PR1) & j <= len PR1 ) by A13, FINSEQ_1:3, XXREAL_0:2;
then ( i in dom PR1 & j in dom PR1 ) by A13, A17, FINSEQ_3:27;
then ( PR1 . i = (PR ^ PR1) . ((len PR) + i) & PR1 . j = (PR ^ PR1) . ((len PR) + j) ) by FINSEQ_1:def 7;
hence ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A3, A14, A15, A16; :: thesis: verum

end;

case ((PR ^ PR1) . (n + (len PR))) `2 = 5 ; :: thesis: ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . (n + (len PR))) `1 )

then consider i, j being Element of NAT , f, g being FinSequence of CQC-WFF such that
A18: ( 1 <= i & i < n & 1 <= j & j < i ) and
A19: ( Ant f = Ant g & f = (PR1 . j) `1 & g = (PR1 . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR1 . n) `1 ) by A2, A3, Def7;
A20: ( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A18, NAT_1:12, XREAL_1:8;
A21: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A18, NAT_1:12, XREAL_1:8;
A22: ( i <= len PR1 & j <= n ) by A1, A18, XXREAL_0:2;
then ( i in Seg (len PR1) & j <= len PR1 ) by A18, FINSEQ_1:3, XXREAL_0:2;
then ( i in dom PR1 & j in dom PR1 ) by A18, A22, FINSEQ_3:27;
then ( PR1 . i = (PR ^ PR1) . ((len PR) + i) & PR1 . j = (PR ^ PR1) . ((len PR) + j) ) by FINSEQ_1:def 7;
hence ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A3, A19, A20, A21; :: thesis: verum

end;

case ((PR ^ PR1) . (n + (len PR))) `2 = 6 ; :: thesis: ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 )

then consider i being Element of NAT , f being FinSequence of CQC-WFF , p, q being Element of CQC-WFF such that
A23: ( 1 <= i & i < n ) and
A24: ( p '&' q = Suc f & f = (PR1 . i) `1 & (Ant f) ^ <*p*> = (PR1 . n) `1 ) by A2, A3, Def7;
A25: ( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A23, NAT_1:12, XREAL_1:8;
i <= len PR1 by A1, A23, XXREAL_0:2;
then i in dom PR1 by A23, FINSEQ_3:27;
then PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
hence ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A3, A24, A25; :: thesis: verum

end;

case ((PR ^ PR1) . (n + (len PR))) `2 = 7 ; :: thesis: ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . (n + (len PR))) `1 )

then consider i being Element of NAT , f being FinSequence of CQC-WFF , p, q being Element of CQC-WFF such that
A26: ( 1 <= i & i < n ) and
A27: ( p '&' q = Suc f & f = (PR1 . i) `1 & (Ant f) ^ <*q*> = (PR1 . n) `1 ) by A2, A3, Def7;
A28: ( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A26, NAT_1:12, XREAL_1:8;
i <= len PR1 by A1, A26, XXREAL_0:2;
then i in dom PR1 by A26, FINSEQ_3:27;
then PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
hence ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A3, A27, A28; :: thesis: verum

end;

case ((PR ^ PR1) . (n + (len PR))) `2 = 8 ; :: thesis: ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n + (len PR) & Suc f = All x,p & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . x,y)*> = ((PR ^ PR1) . (n + (len PR))) `1 )

then consider i being Element of NAT , f being FinSequence of CQC-WFF , p being Element of CQC-WFF , x, y being bound_QC-variable such that
A29: ( 1 <= i & i < n ) and
A30: ( Suc f = All x,p & f = (PR1 . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR1 . n) `1 ) by A2, A3, Def7;
A31: ( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A29, NAT_1:12, XREAL_1:8;
i <= len PR1 by A1, A29, XXREAL_0:2;
then i in dom PR1 by A29, FINSEQ_3:27;
then PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
hence ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n + (len PR) & Suc f = All x,p & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . x,y)*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A3, A30, A31; :: thesis: verum

end;

case ((PR ^ PR1) . (n + (len PR))) `2 = 9 ; :: thesis: ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n + (len PR) & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All x,p)*> = ((PR ^ PR1) . (n + (len PR))) `1 )

then consider i being Element of NAT , f being FinSequence of CQC-WFF , p being Element of CQC-WFF , x, y being bound_QC-variable such that
A32: ( 1 <= i & i < n ) and
A33: ( Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR1 . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR1 . n) `1 ) by A2, A3, Def7;
A34: ( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A32, NAT_1:12, XREAL_1:8;
i <= len PR1 by A1, A32, XXREAL_0:2;
then i in dom PR1 by A32, FINSEQ_3:27;
then PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
hence ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n + (len PR) & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All x,p)*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A3, A33, A34; :: thesis: verum

end;

end;