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
let a be object ; :: thesis: ( a in rng <*[f,0]*> implies a in )
assume a in rng <*[f,0]*> ; :: thesis:
then A2: a = [f,0] by ;
f in set_of_CQC-WFF-seq Al by Def6;
hence a in by ; :: thesis: verum
end;
then rng <*[f,0]*> c= ;
then reconsider PR = <*[f,0]*> as FinSequence of 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:
n <= 1 by ;
then n = 1 by ;
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 ; :: 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