let Al be QC-alphabet ; :: thesis: for n being Nat
for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st 1 <= n & n <= len PR holds
(PR . n) `1 is FinSequence of CQC-WFF Al
let n be Nat; :: thesis: for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st 1 <= n & n <= len PR holds
(PR . n) `1 is FinSequence of CQC-WFF Al
let PR be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; :: thesis: ( 1 <= n & n <= len PR implies (PR . n) `1 is FinSequence of CQC-WFF Al )
assume ( 1 <= n & n <= len PR ) ; :: thesis: (PR . n) `1 is FinSequence of CQC-WFF Al
then n in dom PR by FINSEQ_3:25;
then PR . n in rng PR by FUNCT_1:def 3;
then (PR . n) `1 in set_of_CQC-WFF-seq Al by MCART_1:10;
hence (PR . n) `1 is FinSequence of CQC-WFF Al by Def6; :: thesis: verum