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_1:def 3;

A2: now

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:27;
A5: i in Seg (len b1) by A3, FINSEQ_1:3;
i in dom (AutMt (id V1),b1,b1) by A1, A3, FINSEQ_3:27;
hence (AutMt (id V1),b1,b1) . i = (AutMt (id V1),b1,b1) /. i by PARTFUN1:def 8
.= ((id V1) . (b1 /. i)) |-- b1 by A4, MATRLIN:def 10
.= (b1 /. i) |-- b1 by FUNCT_1:34
.= Line (1. K,(len b1)),i by A4, Th19
.= (1. K,(len b1)) . i by A5, MATRIX_2:10 ;
:: thesis: verum

end;

len (1. K,(len b1)) = len b1 by MATRIX_1:def 3;
hence AutMt (id V1),b1,b1 = 1. K,(len b1) by A1, A2, FINSEQ_1:18; :: thesis: verum