:: deftheorem defines -th_EF GOEDCPUC:def 10 :
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for k being Nat holds k -th_EF (Al,PHI) = the EF-Sequence of Al,PHI . k;