let f be FinSequence of CQC-WFF ; :: thesis: |- f ^ <*VERUM*>
set PR = <*[(f ^ <*VERUM*>),1]*>;
A1: rng <*[(f ^ <*VERUM*>),1]*> = {[(f ^ <*VERUM*>),1]} by FINSEQ_1:38;

now

let a be set ; :: thesis: ( a in rng <*[(f ^ <*VERUM*>),1]*> implies a in [:set_of_CQC-WFF-seq,Proof_Step_Kinds:] )
assume a in rng <*[(f ^ <*VERUM*>),1]*> ; :: thesis: a in [:set_of_CQC-WFF-seq,Proof_Step_Kinds:]
then A2: a = [(f ^ <*VERUM*>),1] by A1, TARSKI:def 1;
f ^ <*VERUM*> in set_of_CQC-WFF-seq by CALCUL_1:def 6;
hence a in [:set_of_CQC-WFF-seq,Proof_Step_Kinds:] by A2, CQC_THE1:21, ZFMISC_1:87; :: thesis: verum

end;

then rng <*[(f ^ <*VERUM*>),1]*> c= [:set_of_CQC-WFF-seq,Proof_Step_Kinds:] by TARSKI:def 3;
then reconsider PR = <*[(f ^ <*VERUM*>),1]*> as FinSequence of [:set_of_CQC-WFF-seq,Proof_Step_Kinds:] by FINSEQ_1:def 4;

now

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*>),1] by FINSEQ_1:40;
then ( (PR . n) `1 = f ^ <*VERUM*> & (PR . n) `2 = 1 ) by MCART_1:7;
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*>),1] by FINSEQ_1:40;
then PR . (len PR) = [(f ^ <*VERUM*>),1] by FINSEQ_1:40;
then (PR . (len PR)) `1 = f ^ <*VERUM*> by MCART_1:7;
hence |- f ^ <*VERUM*> by A5, CALCUL_1:def 9; :: thesis: verum