let V be free finite-rank Z_Module; :: thesis: 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).| = 1
let b1, b2 be OrdBasis of V; :: thesis: for M being Matrix of rank V,F_Real st M = AutMt ((id V),b1,b2) holds
|.(Det M).| = 1
let M be Matrix of rank V,F_Real; :: thesis: ( M = AutMt ((id V),b1,b2) implies |.(Det M).| = 1 )
assume M = AutMt ((id V),b1,b2) ; :: thesis: |.(Det M).| = 1
then ( Det M = 1 or Det M = - 1 ) by ThSign2;
then ( |.(Det M).| = 1 or |.(Det M).| = - (- 1) ) by ABSVALUE:def 1;
hence |.(Det M).| = 1 ; :: thesis: verum