for CS being CongrSpace
for f, g being Permutation of the carrier of CS st f is_DIL_of CS & g is_DIL_of CS holds
f * g is_DIL_of CS