theorem Th37: :: MATRTOP3:37

for n being Nat
for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is rotation holds
( Det (AutMt f) = 1. F_Real iff f is base_rotation )