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

now

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

end;

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

now

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

A9: now

A10: 1 <= len PR by A7, Th6;
then len PR in dom PR by FINSEQ_3:25;
then A11: f = (PR2 . (len PR)) `1 by A4, FINSEQ_1:def 7;
given k being Nat such that A12: k in dom PR1 and
A13: n = (len PR) + k ; :: thesis: PR2,n is_a_correct_step
k in Seg 1 by A12, FINSEQ_1:38;
then A14: k = 1 by FINSEQ_1:2, TARSKI:def 1;
then A15: PR1 . k = [((Ant f) ^ <*p*>),6] by FINSEQ_1:40;
then (PR1 . k) `1 = (Ant f) ^ <*p*> by MCART_1:7;
then A16: (PR2 . n) `1 = (Ant f) ^ <*p*> by A12, A13, FINSEQ_1:def 7;
(PR1 . k) `2 = 6 by A15, MCART_1:7;
then A17: (PR2 . n) `2 = 6 by A12, A13, FINSEQ_1:def 7;
len PR < n by A13, A14, NAT_1:13;
hence PR2,n is_a_correct_step by A1, A16, A17, A10, A11, Def7; :: thesis: verum

end;

now

assume n in dom PR ; :: thesis: PR2,n is_a_correct_step
then A18: ( 1 <= n & n <= len PR ) by FINSEQ_3:25;
then PR,n is_a_correct_step by A3, Def8;
hence PR2,n is_a_correct_step by A18, Th34; :: thesis: verum

end;

hence PR2,n is_a_correct_step by A8, A9, FINSEQ_1:25; :: thesis: verum

end;

then A19: PR2 is a_proof by Def8;
PR2 . (len PR2) = PR2 . ((len PR) + (len PR1)) by FINSEQ_1:22;
then PR2 . (len PR2) = PR2 . ((len PR) + 1) by FINSEQ_1:39;
then PR2 . (len PR2) = PR1 . 1 by A6, FINSEQ_1:def 7;
then PR2 . (len PR2) = [((Ant f) ^ <*p*>),6] by FINSEQ_1:40;
then (PR2 . (len PR2)) `1 = (Ant f) ^ <*p*> by MCART_1:7;
hence |- (Ant f) ^ <*p*> by A19, Def9; :: thesis: verum