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 A2: a in rng <*[(f ^ <*VERUM *>),1]*> ; :: thesis: a in [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :]
A3: a = [(f ^ <*VERUM *>),1] by A1, A2, TARSKI:def 1;
( f ^ <*VERUM *> in set_of_CQC-WFF-seq & 1 in Proof_Step_Kinds ) by CALCUL_1:def 6, CQC_THE1:43;
hence a in [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] by A3, 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 A4: ( 1 <= n & n <= len PR ) ; :: thesis: PR,n is_a_correct_step
( 1 <= n & n <= 1 ) by A4, FINSEQ_1:56;
then n = 1 by 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