theorem :: QC_LANG3:31

for A being QC-alphabet
for a being free_QC-variable of A ex i being Nat st A a. i = a