let i be Nat; :: thesis: for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 st i in dom b1 holds
(b1 /. i) |-- b1 = Line (1. K,(len b1)),i
let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 st i in dom b1 holds
(b1 /. i) |-- b1 = Line (1. K,(len b1)),i
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1 st i in dom b1 holds
(b1 /. i) |-- b1 = Line (1. K,(len b1)),i
let b1 be OrdBasis of V1; :: thesis: ( i in dom b1 implies (b1 /. i) |-- b1 = Line (1. K,(len b1)),i )
set ONE = 1. K,(len b1);
set bb = (b1 /. i) |-- b1;
consider KL being Linear_Combination of V1 such that
A1: ( b1 /. i = Sum KL & Carrier KL c= rng b1 ) and
A2: for k being Nat st 1 <= k & k <= len ((b1 /. i) |-- b1) holds
((b1 /. i) |-- b1) /. k = KL . (b1 /. k) by MATRLIN:def 9;
reconsider rb1 = rng b1 as Basis of V1 by MATRLIN:def 4;
A3: rb1 is linearly-independent by VECTSP_7:def 3;
b1 /. i in {(b1 /. i)} by TARSKI:def 1;
then b1 /. i in Lin {(b1 /. i)} by VECTSP_7:13;
then consider Lb being Linear_Combination of {(b1 /. i)} such that
A4: b1 /. i = Sum Lb by VECTSP_7:12;
assume A5: i in dom b1 ; :: thesis: (b1 /. i) |-- b1 = Line (1. K,(len b1)),i
then A6: b1 . i = b1 /. i by PARTFUN1:def 8;
then A7: Carrier Lb c= {(b1 . i)} by VECTSP_6:def 7;
A8: b1 . i in rb1 by A5, FUNCT_1:def 5;
then {(b1 . i)} c= rb1 by ZFMISC_1:37;
then Carrier Lb c= rb1 by A7, XBOOLE_1:1;
then A9: Lb = KL by A4, A1, A3, MATRLIN:9;
A10: width (1. K,(len b1)) = len b1 by MATRIX_1:25;
A11: Indices (1. K,(len b1)) = [:(Seg (len b1)),(Seg (len b1)):] by MATRIX_1:25;
A12: len b1 = len ((b1 /. i) |-- b1) by MATRLIN:def 9;
A13: b1 /. i <> 0. V1 by A6, A3, A8, VECTSP_7:3;

A14: now

let j be Nat; :: thesis: ( 1 <= j & j <= len ((b1 /. i) |-- b1) implies (Line (1. K,(len b1)),i) . j = ((b1 /. i) |-- b1) . j )
assume A15: ( 1 <= j & j <= len ((b1 /. i) |-- b1) ) ; :: thesis: (Line (1. K,(len b1)),i) . j = ((b1 /. i) |-- b1) . j
A16: j in Seg (len b1) by A12, A15, FINSEQ_1:3;
i in Seg (len b1) by A5, FINSEQ_1:def 3;
then A17: [i,j] in Indices (1. K,(len b1)) by A11, A16, ZFMISC_1:106;
A18: j in dom b1 by A12, A15, FINSEQ_3:27;
A19: dom ((b1 /. i) |-- b1) = dom b1 by A12, FINSEQ_3:31;

now

per cases ( i = j or i <> j ) ;

suppose A20: i = j ; :: thesis: (Line (1. K,(len b1)),i) . j = ((b1 /. i) |-- b1) . j

(Lb . (b1 /. i)) * (b1 /. i) = b1 /. i by A4, VECTSP_6:43
.= (1_ K) * (b1 /. i) by VECTSP_1:def 29 ;
then A21: 1_ K = KL . (b1 /. i) by A13, A9, VECTSP10:5
.= ((b1 /. i) |-- b1) /. j by A2, A15, A20 ;
1_ K = (1. K,(len b1)) * i,j by A17, A20, MATRIX_1:def 12
.= (Line (1. K,(len b1)),i) . j by A10, A16, MATRIX_1:def 8 ;
hence (Line (1. K,(len b1)),i) . j = ((b1 /. i) |-- b1) . j by A18, A19, A21, PARTFUN1:def 8; :: thesis: verum

end;

suppose A22: i <> j ; :: thesis: (Line (1. K,(len b1)),i) . j = ((b1 /. i) |-- b1) . j

b1 is one-to-one by MATRLIN:def 4;
then b1 . i <> b1 . j by A5, A18, A22, FUNCT_1:def 8;
then A23: not b1 . j in Carrier Lb by A7, TARSKI:def 1;
A24: 0. K = (1. K,(len b1)) * i,j by A17, A22, MATRIX_1:def 12
.= (Line (1. K,(len b1)),i) . j by A10, A16, MATRIX_1:def 8 ;
b1 . j = b1 /. j by A18, PARTFUN1:def 8;
then 0. K = KL . (b1 /. j) by A9, A23
.= ((b1 /. i) |-- b1) /. j by A2, A15 ;
hence (Line (1. K,(len b1)),i) . j = ((b1 /. i) |-- b1) . j by A18, A19, A24, PARTFUN1:def 8; :: thesis: verum

end;

end;

end;

hence (Line (1. K,(len b1)),i) . j = ((b1 /. i) |-- b1) . j ; :: thesis: verum

end;

len (Line (1. K,(len b1)),i) = len b1 by A10, FINSEQ_1:def 18;
hence (b1 /. i) |-- b1 = Line (1. K,(len b1)),i by A12, A14, FINSEQ_1:18; :: thesis: verum