for Al being QC-alphabet
for k being Nat holds FCEx (k -th_FCEx Al) = (k + 1) -th_FCEx Al