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

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 A12: ( 1 <= j & j <= len ((b1 /. i) |-- b1) ) ; :: thesis: (Line (1. K,(len b1)),i) . j = ((b1 /. i) |-- b1) . j
A13: ( j in Seg (len b1) & i in Seg (len b1) & j in dom b1 & dom ((b1 /. i) |-- b1) = dom b1 ) by A1, A12, A6, FINSEQ_1:3, FINSEQ_1:def 3, FINSEQ_3:27, FINSEQ_3:31;
then A14: [i,j] in Indices (1. K,(len b1)) by A10, ZFMISC_1:106;

now

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

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

then A16: 1_ K = (1. K,(len b1)) * i,j by A14, MATRIX_1:def 12
.= (Line (1. K,(len b1)),i) . j by A10, A13, MATRIX_1:def 8 ;
(Lb . (b1 /. i)) * (b1 /. i) = b1 /. i by A3, VECTSP_6:43
.= (1_ K) * (b1 /. i) by VECTSP_1:def 26 ;
then 1_ K = KL . (b1 /. i) by A9, A8, VECTSP10:5
.= ((b1 /. i) |-- b1) /. j by A5, A12, A15 ;
hence (Line (1. K,(len b1)),i) . j = ((b1 /. i) |-- b1) . j by A13, A16, PARTFUN1:def 8; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence (b1 /. i) |-- b1 = Line (1. K,(len b1)),i by A6, A11, FINSEQ_1:18; :: thesis: verum