theorem Th6: :: GOEDCPUC:6

for Al being QC-alphabet
for k, n being Element of NAT st n <= k holds
n -th_FCEx Al c= k -th_FCEx Al