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