let V be free finite-rank Z_Module; :: thesis: for b1, b2 being OrdBasis of V holds AutMt ((id V),b1,b2) is Matrix of rank V,INT.Ring
let b1, b2 be OrdBasis of V; :: thesis: AutMt ((id V),b1,b2) is Matrix of rank V,INT.Ring
set n = rank V;
A1: len b1 = rank V by ThRank1;
A2: len b2 = rank V by ThRank1;
P0: len (AutMt ((id V),b1,b2)) = len b1 by Def8;
per cases ( len b1 = 0 or 0 < len b1 ) ;
suppose X1: len b1 = 0 ; :: thesis: AutMt ((id V),b1,b2) is Matrix of rank V,INT.Ring
then len (AutMt ((id V),b1,b2)) = 0 by Def8;
then AutMt ((id V),b1,b2) = {} ;
hence AutMt ((id V),b1,b2) is Matrix of rank V,INT.Ring by A1, X1, MATRIX_0:13; :: thesis: verum
end;
suppose P1: 0 < len b1 ; :: thesis: AutMt ((id V),b1,b2) is Matrix of rank V,INT.Ring
then width (AutMt ((id V),b1,b2)) = len b2 by Th39;
hence AutMt ((id V),b1,b2) is Matrix of rank V,INT.Ring by P0, P1, A1, A2, MATRIX_0:20; :: thesis: verum
end;
end;