let K be Field; :: thesis: for V2 being finite-dimensional VectSp of K
for b2 being OrdBasis of V2
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. K,(len b2)) holds
for v1 being Vector of ((len b2) -VectSp_over K) holds v1 |-- M = v1
let V2 be finite-dimensional VectSp of K; :: thesis: for b2 being OrdBasis of V2
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. K,(len b2)) holds
for v1 being Vector of ((len b2) -VectSp_over K) holds v1 |-- M = v1
let b2 be OrdBasis of V2; :: thesis: for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. K,(len b2)) holds
for v1 being Vector of ((len b2) -VectSp_over K) holds v1 |-- M = v1
let M be OrdBasis of (len b2) -VectSp_over K; :: thesis: ( M = MX2FinS (1. K,(len b2)) implies for v1 being Vector of ((len b2) -VectSp_over K) holds v1 |-- M = v1 )
assume A1: M = MX2FinS (1. K,(len b2)) ; :: thesis: for v1 being Vector of ((len b2) -VectSp_over K) holds v1 |-- M = v1
let v1 be Vector of ((len b2) -VectSp_over K); :: thesis: v1 |-- M = v1
set vM = v1 |-- M;
consider KL being Linear_Combination of (len b2) -VectSp_over K such that
A2: ( v1 = Sum KL & Carrier KL c= rng M ) and
A3: for k being Nat st 1 <= k & k <= len (v1 |-- M) holds
(v1 |-- M) /. k = KL . (M /. k) by MATRLIN:def 9;
reconsider t1 = v1 as Element of (len b2) -tuples_on the carrier of K by MATRIX13:102;
A4: ( len t1 = len b2 & len (v1 |-- M) = len M & len M = dim ((len b2) -VectSp_over K) & dim ((len b2) -VectSp_over K) = len b2 ) by Th21, FINSEQ_1:def 18, MATRIX13:112, MATRLIN:def 9;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len t1 implies t1 . i = (v1 |-- M) . i )
assume A5: ( 1 <= i & i <= len t1 ) ; :: thesis: t1 . i = (v1 |-- M) . i
set F = FinS2MX (KL (#) M);
A6: i in Seg (len b2) by A4, A5, FINSEQ_1:3;
A7: the_rank_of (1. K,(len b2)) = len b2 by Lm6;
A8: ( len (FinS2MX (KL (#) M)) = len M & len (Col (FinS2MX (KL (#) M)),i) = len (FinS2MX (KL (#) M)) ) by FINSEQ_1:def 18, VECTSP_6:def 8;
then A9: ( i in dom (Col (FinS2MX (KL (#) M)),i) & dom (Col (FinS2MX (KL (#) M)),i) = dom (FinS2MX (KL (#) M)) & dom (FinS2MX (KL (#) M)) = dom M & dom M = dom (v1 |-- M) & width (FinS2MX (KL (#) M)) = len b2 ) by A4, A5, FINSEQ_3:27, FINSEQ_3:31, MATRIX_1:25;
then A10: (Col (FinS2MX (KL (#) M)),i) . i = (FinS2MX (KL (#) M)) * i,i by MATRIX_1:def 9
.= (Line (FinS2MX (KL (#) M)),i) . i by A6, A9, MATRIX_1:def 8 ;
A11: M /. i = M . i by A9, PARTFUN1:def 8
.= Line (1. K,(len b2)),i by A1, A6, MATRIX_2:10 ;
A12: ( width (1. K,(len b2)) = len b2 & Indices (1. K,(len b2)) = [:(Seg (len b2)),(Seg (len b2)):] & [i,i] in [:(Seg (len b2)),(Seg (len b2)):] ) by A6, MATRIX_1:25, ZFMISC_1:106;
then A13: (Line (1. K,(len b2)),i) . i = (1. K,(len b2)) * i,i by A6, MATRIX_1:def 8
.= 1_ K by A12, MATRIX_1:def 12 ;
Line (FinS2MX (KL (#) M)),i = (KL (#) M) . i by A6, A4, A8, MATRIX_2:10
.= (KL . (M /. i)) * (M /. i) by A9, VECTSP_6:def 8 ;
then A14: (Col (FinS2MX (KL (#) M)),i) . i = ((KL . (M /. i)) * (Line (1. K,(len b2)),i)) . i by A10, A11, A12, MATRIX13:102
.= (KL . (M /. i)) * (1_ K) by A6, A12, A13, FVSUM_1:63
.= KL . (M /. i) by VECTSP_1:def 13 ;

now

let j be Nat; :: thesis: ( j in dom (Col (FinS2MX (KL (#) M)),i) & j <> i implies (Col (FinS2MX (KL (#) M)),i) . j = 0. K )
assume A15: ( j in dom (Col (FinS2MX (KL (#) M)),i) & j <> i ) ; :: thesis: (Col (FinS2MX (KL (#) M)),i) . j = 0. K
A16: dom (Col (FinS2MX (KL (#) M)),i) = Seg (len b2) by A8, A4, FINSEQ_1:def 3;
A17: (Col (FinS2MX (KL (#) M)),i) . j = (FinS2MX (KL (#) M)) * j,i by A15, A9, MATRIX_1:def 9
.= (Line (FinS2MX (KL (#) M)),j) . i by A6, A9, MATRIX_1:def 8 ;
A18: M /. j = M . j by A9, A15, PARTFUN1:def 8
.= Line (1. K,(len b2)),j by A1, A15, A16, MATRIX_2:10 ;
A19: [j,i] in [:(Seg (len b2)),(Seg (len b2)):] by A6, A15, A16, ZFMISC_1:106;
A20: (Line (1. K,(len b2)),j) . i = (1. K,(len b2)) * j,i by A6, A12, MATRIX_1:def 8
.= 0. K by A19, A15, A12, MATRIX_1:def 12 ;
Line (FinS2MX (KL (#) M)),j = (KL (#) M) . j by A4, A8, A15, A16, MATRIX_2:10
.= (KL . (M /. j)) * (M /. j) by A9, A15, VECTSP_6:def 8 ;
hence (Col (FinS2MX (KL (#) M)),i) . j = ((KL . (M /. j)) * (Line (1. K,(len b2)),j)) . i by A17, A12, A18, MATRIX13:102
.= (KL . (M /. j)) * (0. K) by A6, A12, A20, FVSUM_1:63
.= 0. K by VECTSP_1:36 ;
:: thesis: verum

end;

then (Col (FinS2MX (KL (#) M)),i) . i = Sum (Col (FinS2MX (KL (#) M)),i) by A9, MATRIX_3:14
.= v1 . i by A1, A2, A6, A7, MATRIX13:105, MATRIX13:107 ;
hence t1 . i = (v1 |-- M) /. i by A3, A4, A5, A14
.= (v1 |-- M) . i by A9, PARTFUN1:def 8 ;
:: thesis: verum

end;

hence v1 |-- M = v1 by A4, FINSEQ_1:18; :: thesis: verum