theorem :: TRANSGEO:89

for AFS being AffinSpace
for f, g being Permutation of the carrier of AFS st f is collineation & g is collineation holds
( f " is collineation & f * g is collineation & id the carrier of AFS is collineation )