theorem :: TRANSGEO:37

for OAS being OAffinSpace
for f being Permutation of the carrier of (Lambda OAS) st f is_DIL_of Lambda OAS holds
ex f9 being Permutation of the carrier of OAS st
( f = f9 & f9 is dilatation )