theorem :: TRANSGEO:30

for OAS being OAffinSpace
for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is positive_dilatation holds
f * g is positive_dilatation