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 holds
( not M = AutMt ((id V),b1,b2) or ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )
let b1, b2 be OrdBasis of V; :: thesis: 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 ) )
let M be Matrix of rank V,F_Real; :: thesis: ( not M = AutMt ((id V),b1,b2) or ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )
assume AS1: M = AutMt ((id V),b1,b2) ; :: thesis: ( ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )
set n = rank V;

per cases ( rank V = 0 or rank V > 0 ) ;

suppose AS1: rank V = 0 ; :: thesis: ( ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )

then A1: Det M = 1. F_Real by MATRIXR2:41
.= 1 ;
Det (M @) = 1. F_Real by AS1, MATRIXR2:41
.= 1 ;
hence ( ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) ) by A1; :: thesis: verum

end;

suppose AS2: rank V > 0 ; :: thesis: ( ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )

B0: len b1 = rank V by ZMATRLIN:49;
B1: len (AutMt ((id V),b2,b1)) = len b2 by ZMATRLIN:def 8
.= rank V by ZMATRLIN:49 ;
len b2 = rank V by ZMATRLIN:49;
then width (AutMt ((id V),b2,b1)) = len b1 by AS2, ZMATRLIN:34;
then reconsider M2 = AutMt ((id V),b2,b1) as Matrix of rank V,INT.Ring by AS2, B0, B1, MATRIX_0:20;
( AutMt ((id V),b1,b2) is Matrix of rank V,INT.Ring & AutMt ((id V),b2,b1) is Matrix of rank V,INT.Ring ) by ZMATRLIN:50;
then A1: M * (inttorealM M2) = (AutMt ((id V),b1,b2)) * (AutMt ((id V),b2,b1)) by AS1, AS2, MLT1
.= 1. (INT.Ring,(rank V)) by ZMATRLIN:54, AS2
.= 1. (F_Real,(rank V)) by MLT2 ;
then reconsider MM2 = M * (inttorealM M2) as Matrix of rank V,F_Real ;
A2: (Det M) * (Det (inttorealM M2)) = Det MM2 by MATRIXR2:45
.= 1_ F_Real by AS2, A1, NAT_1:14, MATRIX_7:16
.= 1 ;
reconsider i = Det M as Integer by AS1, ZMATRLIN:51, INT_1:def 2;
Det (inttorealM M2) in INT by ZMATRLIN:51;
then reconsider j = Det (inttorealM M2) as Integer ;
i * j = 1 by A2;
then ( Det M = 1 or Det M = - 1 ) by INT_1:9;
hence ( ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) ) by AS2, MATRIX_7:37, NAT_1:14; :: thesis: verum

end;

end;