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;

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

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

|- 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:]

then
rng <*[f,0]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
;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;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

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

then A6:
PR is a_proof
;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;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

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