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:38;

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:21, ZFMISC_1:87; :: 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:39;
then n = 1 by A4, XXREAL_0:1;
then PR . n = [f,0] by FINSEQ_1:40;
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:40;
then PR . (len PR) = [f,0] by FINSEQ_1:40;
then (PR . (len PR)) `1 = f by MCART_1:7;
hence |- f by A6, Def9; :: thesis: verum