for A being set
for K being Element of Normal_forms_on A holds mi (K ^ K) = K