let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable
for f being FinSequence of CQC-WFF st Suc f = All x,p & |- f holds
|- (Ant f) ^ <*(p . x,y)*>
let x, y be bound_QC-variable; :: thesis: for f being FinSequence of CQC-WFF st Suc f = All x,p & |- f holds
|- (Ant f) ^ <*(p . x,y)*>
let f be FinSequence of CQC-WFF ; :: thesis: ( Suc f = All x,p & |- f implies |- (Ant f) ^ <*(p . x,y)*> )
assume A1: ( Suc f = All x,p & |- f ) ; :: thesis: |- (Ant f) ^ <*(p . x,y)*>
then consider PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] such that
A2: ( PR is a_proof & (PR . (len PR)) `1 = f ) by Def9;
A3: ( (Ant f) ^ <*(p . x,y)*> in set_of_CQC-WFF-seq & 8 in Proof_Step_Kinds ) by Def6, CQC_THE1:43;

now

let a be set ; :: thesis: ( a in rng <*[((Ant f) ^ <*(p . x,y)*>),8]*> implies a in [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] )
assume A4: a in rng <*[((Ant f) ^ <*(p . x,y)*>),8]*> ; :: thesis: a in [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :]
a in {[((Ant f) ^ <*(p . x,y)*>),8]} by A4, FINSEQ_1:55;
then a = [((Ant f) ^ <*(p . x,y)*>),8] by TARSKI:def 1;
hence a in [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] by A3, ZFMISC_1:106; :: thesis: verum

end;

then rng <*[((Ant f) ^ <*(p . x,y)*>),8]*> c= [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] by TARSKI:def 3;
then reconsider PR1 = <*[((Ant f) ^ <*(p . x,y)*>),8]*> as FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] by FINSEQ_1:def 4;
set PR2 = PR ^ PR1;
reconsider PR2 = PR ^ PR1 as FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] ;
A5: PR <> {} by A2, Def8;

now

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

A9: now

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

end;

now

given k being Nat such that A11: ( k in dom PR1 & n = (len PR) + k ) ; :: thesis: PR2,n is_a_correct_step
k in Seg 1 by A11, FINSEQ_1:55;
then A12: k = 1 by FINSEQ_1:4, TARSKI:def 1;
then PR1 . k = [((Ant f) ^ <*(p . x,y)*>),8] by FINSEQ_1:57;
then ( (PR1 . k) `1 = (Ant f) ^ <*(p . x,y)*> & (PR1 . k) `2 = 8 ) by MCART_1:7;
then A13: ( (PR2 . n) `1 = (Ant f) ^ <*(p . x,y)*> & (PR2 . n) `2 = 8 ) by A11, FINSEQ_1:def 7;
A14: ( 1 <= len PR & len PR < n ) by A5, A11, A12, Th6, NAT_1:13;
then len PR in dom PR by FINSEQ_3:27;
then f = (PR2 . (len PR)) `1 by A2, FINSEQ_1:def 7;
hence PR2,n is_a_correct_step by A1, A13, A14, Def7; :: thesis: verum

end;

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

end;

then A15: PR2 is a_proof by Def8;
PR2 . (len PR2) = PR2 . ((len PR) + (len PR1)) by FINSEQ_1:35;
then A16: PR2 . (len PR2) = PR2 . ((len PR) + 1) by FINSEQ_1:56;
1 in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
then 1 in dom PR1 by FINSEQ_1:55;
then PR2 . (len PR2) = PR1 . 1 by A16, FINSEQ_1:def 7;
then PR2 . (len PR2) = [((Ant f) ^ <*(p . x,y)*>),8] by FINSEQ_1:57;
then (PR2 . (len PR2)) `1 = (Ant f) ^ <*(p . x,y)*> by MCART_1:7;
hence |- (Ant f) ^ <*(p . x,y)*> by A15, Def9; :: thesis: verum