let V be free finite-rank Z_Module; :: thesis: for b1, b2 being OrdBasis of V st rank V > 0 holds
(AutMt ((id V),b1,b2)) * (AutMt ((id V),b2,b1)) = 1. (INT.Ring,(rank V))
let b1, b2 be OrdBasis of V; :: thesis: ( rank V > 0 implies (AutMt ((id V),b1,b2)) * (AutMt ((id V),b2,b1)) = 1. (INT.Ring,(rank V)) )
assume AS: rank V > 0 ; :: thesis: (AutMt ((id V),b1,b2)) * (AutMt ((id V),b2,b1)) = 1. (INT.Ring,(rank V))
then A1: ( len b1 > 0 & len b2 > 0 ) by ThRank1;
thus (AutMt ((id V),b1,b2)) * (AutMt ((id V),b2,b1)) = AutMt (((id V) * (id V)),b1,b1) by A1, ThComp1
.= AutMt ((id V),b1,b1) by FUNCT_2:17
.= 1. (INT.Ring,(rank V)) by AS, LmSign31 ; :: thesis: verum