theorem Th34: :: CALCUL_1:34

for Al being QC-alphabet
for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
for n being Nat st 1 <= n & n <= len PR holds
( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )