:: deftheorem defines -th_FCEx GOEDCPUC:def 8 :
for Al being QC-alphabet
for k being Nat holds k -th_FCEx Al = the FCEx-Sequence of Al,k . (k + 1);