let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al holds |- f ^ <*(VERUM Al)*>
let f be FinSequence of CQC-WFF Al; :: thesis: |- f ^ <*(VERUM Al)*>
set PR = <*[(f ^ <*(VERUM Al)*>),1]*>;
A1: rng <*[(f ^ <*(VERUM Al)*>),1]*> = {[(f ^ <*(VERUM Al)*>),1]} by FINSEQ_1:38;
now :: thesis: for a being object st a in rng <*[(f ^ <*(VERUM Al)*>),1]*> holds
a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
let a be object ; :: thesis: ( a in rng <*[(f ^ <*(VERUM Al)*>),1]*> implies a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] )
assume a in rng <*[(f ^ <*(VERUM Al)*>),1]*> ; :: thesis: a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
then A2: a = [(f ^ <*(VERUM Al)*>),1] by A1, TARSKI:def 1;
f ^ <*(VERUM Al)*> in set_of_CQC-WFF-seq Al by CALCUL_1:def 6;
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 ^ <*(VERUM Al)*>),1]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;
then reconsider PR = <*[(f ^ <*(VERUM Al)*>),1]*> as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
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
A3: 1 <= n and
A4: n <= len PR ; :: thesis: PR,n is_a_correct_step
n <= 1 by A4, FINSEQ_1:39;
then n = 1 by A3, XXREAL_0:1;
then PR . n = [(f ^ <*(VERUM Al)*>),1] by FINSEQ_1:40;
then ( (PR . n) `1 = f ^ <*(VERUM Al)*> & (PR . n) `2 = 1 ) ;
hence PR,n is_a_correct_step by CALCUL_1:def 7; :: thesis: verum
end;
then A5: PR is a_proof by CALCUL_1:def 8;
PR . 1 = [(f ^ <*(VERUM Al)*>),1] by FINSEQ_1:40;
then PR . (len PR) = [(f ^ <*(VERUM Al)*>),1] by FINSEQ_1:40;
then (PR . (len PR)) `1 = f ^ <*(VERUM Al)*> ;
hence |- f ^ <*(VERUM Al)*> by A5, CALCUL_1:def 9; :: thesis: verum