for i, n being Nat
for f1, f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation & Det (AutMt f1) = - (1. F_Real) & i in Seg n & AutMt f2 = AxialSymmetry (i,n) holds
f1 * f2 is base_rotation