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

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