let n be Element of NAT ; :: thesis: for PR being FinSequence of [:set_of_CQC-WFF-seq,Proof_Step_Kinds:] st 1 <= n & n <= len PR holds
(PR . n) `1 is FinSequence of CQC-WFF
let PR be FinSequence of [:set_of_CQC-WFF-seq,Proof_Step_Kinds:]; :: thesis: ( 1 <= n & n <= len PR implies (PR . n) `1 is FinSequence of CQC-WFF )
assume ( 1 <= n & n <= len PR ) ; :: thesis: (PR . n) `1 is FinSequence of CQC-WFF
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 by MCART_1:10;
hence (PR . n) `1 is FinSequence of CQC-WFF by Def6; :: thesis: verum