theorem Th27: :: CQC_THE1:31

for Al being QC-alphabet
for l being Nat
for X being Subset of (CQC-WFF Al)
for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds
(f . l) `1 in Cn X