theorem Th24: :: CQC_THE1:28

for Al being QC-alphabet
for n being Nat
for X being Subset of (CQC-WFF Al)
for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds
f ^ g,n + (len f) is_a_correct_step_wrt X