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:55;

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:43, ZFMISC_1:106; :: 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:56;
then n = 1 by A3, XXREAL_0:1;
then PR . n = [(f ^ <*VERUM *>),1] by FINSEQ_1:57;
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:57;
then PR . (len PR) = [(f ^ <*VERUM *>),1] by FINSEQ_1:57;
then (PR . (len PR)) `1 = f ^ <*VERUM *> by MCART_1:7;
hence |- f ^ <*VERUM *> by A5, CALCUL_1:def 9; :: thesis: verum