let V be free finite-rank Z_Module; for b1, b2 being OrdBasis of V
for M being Matrix of rank V,F_Real st M = AutMt ((id V),b1,b2) holds
Det M in INT
let b1, b2 be OrdBasis of V; for M being Matrix of rank V,F_Real st M = AutMt ((id V),b1,b2) holds
Det M in INT
let M be Matrix of rank V,F_Real; ( M = AutMt ((id V),b1,b2) implies Det M in INT )
assume A2:
M = AutMt ((id V),b1,b2)
; Det M in INT