for A being set
for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) = (K ^ L) ^ M