let PR, PR1 be FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :]; :: thesis:
let n be Nat; :: thesis:
assume A1: ( 1 <= n & n <= len PR ) ; :: thesis:
then n in dom PR by FINSEQ_3:27;
then A2: (PR ^ PR1) . n = PR . n by FINSEQ_1:def 7;
len (PR ^ PR1) = (len PR) + (len PR1) by FINSEQ_1:35;
then len PR <= len (PR ^ PR1) by NAT_1:11;
then A3: ( 1 <= n & n <= len (PR ^ PR1) ) by A1, XXREAL_0:2;
thus ( PR,n is_a_correct_step implies PR ^ PR1,n is_a_correct_step ) :: thesis:

proof

assume A4: PR,n is_a_correct_step ; :: thesis:

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

case ((PR ^ PR1) . n) `2 = 0 ; :: thesis:

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

end;

case ((PR ^ PR1) . n) `2 = 1 ; :: thesis:

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

end;

case ((PR ^ PR1) . n) `2 = 2 ; :: thesis:

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 & (PR . i) `1 = f & (PR . n) `1 = g ) by A2, A4, Def7;
i <= len PR by A1, A5, XXREAL_0:2;
then i in dom PR by A5, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . n) `1 = g ) by A2, A5, A6; :: thesis:

end;

case ((PR ^ PR1) . n) `2 = 3 ; :: thesis:

then consider i, j being Element of NAT , f, g being FinSequence of CQC-WFF such that
A7: ( 1 <= i & i < n & 1 <= j & j 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) by A2, A4, Def7;
( i <= len PR & j <= n ) by A1, A7, XXREAL_0:2;
then ( i in Seg (len PR) & j <= len PR ) by A7, FINSEQ_1:3, XXREAL_0:2;
then ( i in dom PR & j in dom PR ) by A7, FINSEQ_1:def 3, FINSEQ_3:27;
then ( PR . i = (PR ^ PR1) . i & PR . j = (PR ^ PR1) . 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 & 1 <= j & j 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) `1 ) by A2, A7, A8; :: thesis:

end;

case ((PR ^ PR1) . n) `2 = 4 ; :: thesis:

then consider i, j being Element of NAT , f, g being FinSequence of CQC-WFF , p being Element of CQC-WFF such that
A9: ( 1 <= i & i < n & 1 <= j & j 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) by A2, A4, Def7;
( i <= len PR & j <= n ) by A1, A9, XXREAL_0:2;
then ( i in Seg (len PR) & j <= len PR ) by A9, FINSEQ_1:3, XXREAL_0:2;
then ( i in dom PR & j in dom PR ) by A9, FINSEQ_1:def 3, FINSEQ_3:27;
then ( PR . i = (PR ^ PR1) . i & PR . j = (PR ^ PR1) . 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 & 1 <= j & j 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) `1 ) by A2, A9, A10; :: thesis:

end;

case ((PR ^ PR1) . n) `2 = 5 ; :: thesis:

then consider i, j being Element of NAT , f, g being FinSequence of CQC-WFF such that
A11: ( 1 <= i & i < n & 1 <= j & j = (PR . n) `1 ) by A2, A4, Def7;
( i <= len PR & j <= n ) by A1, A11, XXREAL_0:2;
then ( i in Seg (len PR) & j <= len PR ) by A11, FINSEQ_1:3, XXREAL_0:2;
then ( i in dom PR & j in dom PR ) by A11, FINSEQ_1:def 3, FINSEQ_3:27;
then ( PR . i = (PR ^ PR1) . i & PR . j = (PR ^ PR1) . 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 & 1 <= j & j = ((PR ^ PR1) . n) `1 ) by A2, A11, A12; :: thesis:

end;

case ((PR ^ PR1) . n) `2 = 6 ; :: thesis:

then consider i being Element of NAT , f being FinSequence of CQC-WFF , p, q being Element of CQC-WFF such that
A13: ( 1 <= i & i < n ) and
A14: ( p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) by A2, A4, Def7;
i <= len PR by A1, A13, XXREAL_0:2;
then i in dom PR by A13, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A2, A13, A14; :: thesis:

end;

case ((PR ^ PR1) . n) `2 = 7 ; :: thesis:

then consider i being Element of NAT , f being FinSequence of CQC-WFF , p, q being Element of CQC-WFF such that
A15: ( 1 <= i & i < n ) and
A16: ( p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) by A2, A4, Def7;
i <= len PR by A1, A15, XXREAL_0:2;
then i in dom PR by A15, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 ) by A2, A15, A16; :: thesis:

end;

case ((PR ^ PR1) . n) `2 = 8 ; :: thesis:

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
A17: ( 1 <= i & i < n ) and
A18: ( Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) by A2, A4, Def7;
i <= len PR by A1, A17, XXREAL_0:2;
then i in dom PR by A17, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & Suc f = All x,p & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . x,y)*> = ((PR ^ PR1) . n) `1 ) by A2, A17, A18; :: thesis:

end;

case ((PR ^ PR1) . n) `2 = 9 ; :: thesis:

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
A19: ( 1 <= i & i < n ) and
A20: ( 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 . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) by A2, A4, Def7;
i <= len PR by A1, A19, XXREAL_0:2;
then i in dom PR by A19, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & 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) `1 ) by A2, A19, A20; :: thesis:

end;

assume A21: PR ^ PR1,n is_a_correct_step ; :: thesis:

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

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

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

end;

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

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

end;

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

then consider i being Element of NAT , f, g being FinSequence of CQC-WFF such that
A22: ( 1 <= i & i < n ) and
A23: ( Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . n) `1 = g ) by A2, A21, Def7;
i <= len PR by A1, A22, XXREAL_0:2;
then i in dom PR by A22, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) by A2, A22, A23; :: thesis:

end;

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

then consider i, j being Element of NAT , f, f1 being FinSequence of CQC-WFF such that
A24: ( 1 <= i & i < n & 1 <= j & j 1 & len f1 > 1 & Ant (Ant f) = Ant (Ant f1) & 'not' (Suc (Ant f)) = Suc (Ant f1) & Suc f = Suc f1 & f = ((PR ^ PR1) . j) `1 & f1 = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . n) `1 ) by A2, A21, Def7;
( i <= len PR & j <= n ) by A1, A24, XXREAL_0:2;
then ( i in Seg (len PR) & j <= len PR ) by A24, FINSEQ_1:3, XXREAL_0:2;
then ( i in dom PR & j in dom PR ) by A24, FINSEQ_1:def 3, FINSEQ_3:27;
then ( PR . i = (PR ^ PR1) . i & PR . j = (PR ^ PR1) . 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 & 1 <= j & j 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) by A2, A24, A25; :: thesis:

end;

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

then consider i, j being Element of NAT , f, g being FinSequence of CQC-WFF , p being Element of CQC-WFF such that
A26: ( 1 <= i & i < n & 1 <= j & j 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) `1 ) by A2, A21, Def7;
( i <= len PR & j <= n ) by A1, A26, XXREAL_0:2;
then ( i in Seg (len PR) & j <= len PR ) by A26, FINSEQ_1:3, XXREAL_0:2;
then ( i in dom PR & j in dom PR ) by A26, FINSEQ_1:def 3, FINSEQ_3:27;
then ( PR . i = (PR ^ PR1) . i & PR . j = (PR ^ PR1) . 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 & 1 <= j & j 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) by A2, A26, A27; :: thesis:

end;

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

then consider i, j being Element of NAT , f, g being FinSequence of CQC-WFF such that
A28: ( 1 <= i & i < n & 1 <= j & j = ((PR ^ PR1) . n) `1 ) by A2, A21, Def7;
( i <= len PR & j <= n ) by A1, A28, XXREAL_0:2;
then ( i in Seg (len PR) & j <= len PR ) by A28, FINSEQ_1:3, XXREAL_0:2;
then ( i in dom PR & j in dom PR ) by A28, FINSEQ_1:def 3, FINSEQ_3:27;
then ( PR . i = (PR ^ PR1) . i & PR . j = (PR ^ PR1) . 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 & 1 <= j & j = (PR . n) `1 ) by A2, A28, A29; :: thesis:

end;

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

then consider i being Element of NAT , f being FinSequence of CQC-WFF , p, q being Element of CQC-WFF such that
A30: ( 1 <= i & i < n ) and
A31: ( p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 ) by A2, A21, Def7;
i <= len PR by A1, A30, XXREAL_0:2;
then i in dom PR by A30, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) by A2, A30, A31; :: thesis:

end;

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

then consider i being Element of NAT , f being FinSequence of CQC-WFF , p, q being Element of CQC-WFF such that
A32: ( 1 <= i & i < n ) and
A33: ( p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 ) by A2, A21, Def7;
i <= len PR by A1, A32, XXREAL_0:2;
then i in dom PR by A32, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) by A2, A32, A33; :: thesis:

end;

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

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
A34: ( 1 <= i & i < n ) and
A35: ( Suc f = All x,p & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . x,y)*> = ((PR ^ PR1) . n) `1 ) by A2, A21, Def7;
i <= len PR by A1, A34, XXREAL_0:2;
then i in dom PR by A34, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) by A2, A34, A35; :: thesis:

end;

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

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
A36: ( 1 <= i & i < n ) and
A37: ( 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) `1 ) by A2, A21, Def7;
i <= len PR by A1, A36, XXREAL_0:2;
then i in dom PR by A36, FINSEQ_3:27;
then PR . i = (PR ^ PR1) . 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 & 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 . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) by A2, A36, A37; :: thesis:

end;