let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al st 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & |- f & |- g holds
|- (Ant (Ant f)) ^ <*(Suc f)*>
let f, g be FinSequence of CQC-WFF Al; :: thesis: ( 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & |- f & |- g implies |- (Ant (Ant f)) ^ <*(Suc f)*> )
assume that
A1: ( 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g ) and
A2: |- f and
A3: |- g ; :: thesis: |- (Ant (Ant f)) ^ <*(Suc f)*>
consider PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that
A4: PR1 is a_proof and
A5: g = (PR1 . (len PR1)) `1 by A3;
consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that
A6: PR is a_proof and
A7: f = (PR . (len PR)) `1 by A2;
A8: (Ant (Ant f)) ^ <*(Suc f)*> in set_of_CQC-WFF-seq Al by Def6;

now :: thesis: for a being object st a in rng <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> holds
a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

let a be object ; :: thesis: ( a in rng <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> implies a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] )
assume a in rng <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> ; :: thesis: a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
then a in {[((Ant (Ant f)) ^ <*(Suc f)*>),3]} by FINSEQ_1:38;
then a = [((Ant (Ant f)) ^ <*(Suc f)*>),3] by TARSKI:def 1;
hence a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by A8, CQC_THE1:21, ZFMISC_1:87; :: thesis: verum

end;

then rng <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;
then reconsider PR2 = <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then A9: 1 in dom PR2 by FINSEQ_1:38;
set PR3 = (PR ^ PR1) ^ PR2;
reconsider PR3 = (PR ^ PR1) ^ PR2 as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;
A10: PR <> {} by A6;

now :: thesis: for n being Nat st 1 <= n & n <= len PR3 holds
PR3,n is_a_correct_step

let n be Nat; :: thesis: ( 1 <= n & n <= len PR3 implies PR3,n is_a_correct_step )
assume ( 1 <= n & n <= len PR3 ) ; :: thesis: PR3,n is_a_correct_step
then A11: n in dom PR3 by FINSEQ_3:25;

A12: now :: thesis: ( ex k being Nat st
( k in dom PR2 & n = (len (PR ^ PR1)) + k ) implies PR3,n is_a_correct_step )

given k being Nat such that A13: k in dom PR2 and
A14: n = (len (PR ^ PR1)) + k ; :: thesis: PR3,n is_a_correct_step
k in Seg 1 by A13, FINSEQ_1:38;
then A15: k = 1 by FINSEQ_1:2, TARSKI:def 1;
then A16: PR2 . k = [((Ant (Ant f)) ^ <*(Suc f)*>),3] ;
then (PR2 . k) `1 = (Ant (Ant f)) ^ <*(Suc f)*> ;
then A17: (PR3 . n) `1 = (Ant (Ant f)) ^ <*(Suc f)*> by A13, A14, FINSEQ_1:def 7;
(PR2 . k) `2 = 3 by A16;
then A18: (PR3 . n) `2 = 3 by A13, A14, FINSEQ_1:def 7;
A19: len (PR ^ PR1) < n by A14, A15, NAT_1:13;
A20: 1 <= len PR by A10, Th6;
then len PR in dom PR by FINSEQ_3:25;
then A21: f = ((PR ^ PR1) . (len PR)) `1 by A7, FINSEQ_1:def 7;
A22: PR1 <> {} by A4;
then A23: len PR < len (PR ^ PR1) by Th6;
then len PR in dom (PR ^ PR1) by A20, FINSEQ_3:25;
then A24: f = (PR3 . (len PR)) `1 by A21, FINSEQ_1:def 7;
1 <= len PR1 by A22, Th6;
then len PR1 in dom PR1 by FINSEQ_3:25;
then g = ((PR ^ PR1) . ((len PR) + (len PR1))) `1 by A5, FINSEQ_1:def 7;
then A25: g = ((PR ^ PR1) . (len (PR ^ PR1))) `1 by FINSEQ_1:22;
1 <= len (PR ^ PR1) by A10, Th6;
then len (PR ^ PR1) in dom (PR ^ PR1) by FINSEQ_3:25;
then A26: g = (PR3 . (len (PR ^ PR1))) `1 by A25, FINSEQ_1:def 7;
1 <= len (PR ^ PR1) by A10, Th6;
hence PR3,n is_a_correct_step by A1, A17, A18, A20, A23, A24, A19, A26, Def7; :: thesis: verum

end;

now :: thesis: ( n in dom (PR ^ PR1) implies PR3,n is_a_correct_step )

A27: now :: thesis: ( ex k being Nat st
( k in dom PR1 & n = (len PR) + k ) implies PR3,n is_a_correct_step )

given k being Nat such that A28: k in dom PR1 and
A29: n = (len PR) + k ; :: thesis: PR3,n is_a_correct_step
A30: 1 <= k by A28, FINSEQ_3:25;
A31: k <= len PR1 by A28, FINSEQ_3:25;
then n <= (len PR1) + (len PR) by A29, XREAL_1:6;
then A32: n <= len (PR ^ PR1) by FINSEQ_1:22;
k <= n by A29, NAT_1:11;
then A33: 1 <= n by A30, XXREAL_0:2;
PR1,k is_a_correct_step by A4, A30, A31;
then PR ^ PR1,n is_a_correct_step by A29, A30, A31, Th35;
hence PR3,n is_a_correct_step by A33, A32, Th34; :: thesis: verum

end;

A34: now :: thesis: ( n in dom PR implies PR3,n is_a_correct_step )

assume A35: n in dom PR ; :: thesis: PR3,n is_a_correct_step
then A36: 1 <= n by FINSEQ_3:25;
A37: n <= len PR by A35, FINSEQ_3:25;
len PR <= len (PR ^ PR1) by Th6;
then A38: n <= len (PR ^ PR1) by A37, XXREAL_0:2;
PR,n is_a_correct_step by A6, A36, A37;
then PR ^ PR1,n is_a_correct_step by A36, A37, Th34;
hence PR3,n is_a_correct_step by A36, A38, Th34; :: thesis: verum

end;

assume n in dom (PR ^ PR1) ; :: thesis: PR3,n is_a_correct_step
hence PR3,n is_a_correct_step by A34, A27, FINSEQ_1:25; :: thesis: verum

end;

hence PR3,n is_a_correct_step by A11, A12, FINSEQ_1:25; :: thesis: verum

end;

then A39: PR3 is a_proof ;
PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + (len PR2)) by FINSEQ_1:22;
then PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + 1) by FINSEQ_1:39;
then PR3 . (len PR3) = PR2 . 1 by A9, FINSEQ_1:def 7;
then PR3 . (len PR3) = [((Ant (Ant f)) ^ <*(Suc f)*>),3] ;
then (PR3 . (len PR3)) `1 = (Ant (Ant f)) ^ <*(Suc f)*> ;
hence |- (Ant (Ant f)) ^ <*(Suc f)*> by A39; :: thesis: verum