let Al be QC-alphabet ; for f being FinSequence of CQC-WFF Al holds |- f ^ <*(VERUM Al)*>
let f be FinSequence of CQC-WFF Al; |- f ^ <*(VERUM Al)*>
set PR = <*[(f ^ <*(VERUM Al)*>),1]*>;
A1:
rng <*[(f ^ <*(VERUM Al)*>),1]*> = {[(f ^ <*(VERUM Al)*>),1]}
by FINSEQ_1:38;
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;
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; verum