let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds AutMt ((id V1),b1,b1) = 1. (K,(len b1))
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1 holds AutMt ((id V1),b1,b1) = 1. (K,(len b1))
let b1 be OrdBasis of V1; :: thesis: AutMt ((id V1),b1,b1) = 1. (K,(len b1))
set A = AutMt ((id V1),b1,b1);
set ONE = 1. (K,(len b1));
A1: len (AutMt ((id V1),b1,b1)) = len b1 by MATRIX_0:def 2;

A2: now :: thesis: for i being Nat st 1 <= i & i <= len b1 holds
(AutMt ((id V1),b1,b1)) . i = (1. (K,(len b1))) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len b1 implies (AutMt ((id V1),b1,b1)) . i = (1. (K,(len b1))) . i )
assume A3: ( 1 <= i & i <= len b1 ) ; :: thesis: (AutMt ((id V1),b1,b1)) . i = (1. (K,(len b1))) . i
A4: i in dom b1 by A3, FINSEQ_3:25;
A5: i in Seg (len b1) by A3;
i in dom (AutMt ((id V1),b1,b1)) by A1, A3, FINSEQ_3:25;
hence (AutMt ((id V1),b1,b1)) . i = (AutMt ((id V1),b1,b1)) /. i by PARTFUN1:def 6
.= ((id V1) . (b1 /. i)) |-- b1 by A4, MATRLIN:def 8
.= (b1 /. i) |-- b1
.= Line ((1. (K,(len b1))),i) by A4, Th19
.= (1. (K,(len b1))) . i by A5, MATRIX_0:52 ;
:: thesis: verum

end;

len (1. (K,(len b1))) = len b1 by MATRIX_0:def 2;
hence AutMt ((id V1),b1,b1) = 1. (K,(len b1)) by A1, A2; :: thesis: verum