theorem ThSign2: :: ZMODLAT1:99

for V being free finite-rank Z_Module
for b1, b2 being OrdBasis of V
for M being Matrix of rank V,F_Real holds
( not M = AutMt ((id V),b1,b2) or ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )