let f be FinSequence of CQC-WFF ; :: thesis: ( Suc f is_tail_of Ant f implies |- f )
set PR = <*[f,0 ]*>;
A1: rng <*[f,0 ]*> = {[f,0 ]} by FINSEQ_1:55;

now

let a be set ; :: thesis: ( a in rng <*[f,0 ]*> implies a in [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] )
assume a in rng <*[f,0 ]*> ; :: thesis: a in [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :]
then A2: a = [f,0 ] by A1, TARSKI:def 1;
f in set_of_CQC-WFF-seq by Def6;
hence a in [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] by A2, CQC_THE1:43, ZFMISC_1:106; :: thesis: verum

end;

then rng <*[f,0 ]*> c= [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] by TARSKI:def 3;
then reconsider PR = <*[f,0 ]*> as FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] by FINSEQ_1:def 4;
assume A3: Suc f is_tail_of Ant f ; :: thesis: |- f

now

let n be Nat; :: thesis: ( 1 <= n & n <= len PR implies PR,n is_a_correct_step )
assume that
A4: 1 <= n and
A5: n <= len PR ; :: thesis: PR,n is_a_correct_step
n <= 1 by A5, FINSEQ_1:56;
then n = 1 by A4, XXREAL_0:1;
then PR . n = [f,0 ] by FINSEQ_1:57;
then ( (PR . n) `1 = f & (PR . n) `2 = 0 ) by MCART_1:7;
hence PR,n is_a_correct_step by A3, Def7; :: thesis: verum

end;

then A6: PR is a_proof by Def8;
PR . 1 = [f,0 ] by FINSEQ_1:57;
then PR . (len PR) = [f,0 ] by FINSEQ_1:57;
then (PR . (len PR)) `1 = f by MCART_1:7;
hence |- f by A6, Def9; :: thesis: verum