:: deftheorem Def6 defines Effect CQC_THE1:def 6 :
for Al being QC-alphabet
for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f <> {} holds
Effect f = (f . (len f)) `1 ;