let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al st Suc f is_tail_of Ant f holds
|- f
let f be FinSequence of CQC-WFF Al; :: 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 :: thesis: for a being object st a in rng <*[f,0]*> holds
a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
let a be object ; :: thesis: ( a in rng <*[f,0]*> implies a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] )
assume a in rng <*[f,0]*> ; :: thesis: a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
then A2: a = [f,0] by A1, TARSKI:def 1;
f in set_of_CQC-WFF-seq Al by Def6;
hence a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by A2, CQC_THE1:21, ZFMISC_1:87; :: thesis: verum
end;
then rng <*[f,0]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;
then reconsider PR = <*[f,0]*> as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
assume A3: Suc f is_tail_of Ant f ; :: thesis: |- f
now :: thesis: for n being Nat st 1 <= n & n <= len PR holds
PR,n is_a_correct_step
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 ) ;
hence PR,n is_a_correct_step by A3, Def7; :: thesis: verum
end;
then A6: PR is a_proof ;
PR . 1 = [f,0] by FINSEQ_1:40;
then PR . (len PR) = [f,0] by FINSEQ_1:40;
then (PR . (len PR)) `1 = f ;
hence |- f by A6; :: thesis: verum