theorem Th23: :: CQC_THE1:27

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 f holds
( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )