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 7;
reconsider t1 = v1 as Element of (len b2) -tuples_on the carrier of K by MATRIX13:102;
A4: len t1 = len b2 by CARD_1:def 7;
A5: ( len M = dim ((len b2) -VectSp_over K) & dim ((len b2) -VectSp_over K) = len b2 ) by Th21, MATRIX13:112;
A6: len (v1 |-- M) = len M by MATRLIN:def 7;

now :: thesis: for i being Nat st 1 <= i & i <= len t1 holds
t1 . i = (v1 |-- M) . i

A7: dom M = dom (v1 |-- M) by A6, FINSEQ_3:29;
A8: the_rank_of (1. (K,(len b2))) = len b2 by Lm6;
set F = FinS2MX (KL (#) M);
A9: Indices (1. (K,(len b2))) = [:(Seg (len b2)),(Seg (len b2)):] by MATRIX_0:24;
let i be Nat; :: thesis: ( 1 <= i & i <= len t1 implies t1 . i = (v1 |-- M) . i )
assume A10: ( 1 <= i & i <= len t1 ) ; :: thesis: t1 . i = (v1 |-- M) . i
A11: i in Seg (len b2) by A4, A10;
then A12: [i,i] in [:(Seg (len b2)),(Seg (len b2)):] by ZFMISC_1:87;
A13: width (1. (K,(len b2))) = len b2 by MATRIX_0:24;
then A14: (Line ((1. (K,(len b2))),i)) . i = (1. (K,(len b2))) * (i,i) by A11, MATRIX_0:def 7
.= 1_ K by A9, A12, MATRIX_1:def 3 ;
A15: len (Col ((FinS2MX (KL (#) M)),i)) = len (FinS2MX (KL (#) M)) by CARD_1:def 7;
then A16: dom (Col ((FinS2MX (KL (#) M)),i)) = dom (FinS2MX (KL (#) M)) by FINSEQ_3:29;
A17: len (FinS2MX (KL (#) M)) = len M by VECTSP_6:def 5;
then A18: dom (FinS2MX (KL (#) M)) = dom M by FINSEQ_3:29;
A19: i in dom (Col ((FinS2MX (KL (#) M)),i)) by A4, A5, A10, A17, A15, FINSEQ_3:25;
A20: width (FinS2MX (KL (#) M)) = len b2 by A5, A17, MATRIX_0:24;

now :: thesis: for j being Nat st j in dom (Col ((FinS2MX (KL (#) M)),i)) & j <> i holds
(Col ((FinS2MX (KL (#) M)),i)) . j = 0. K

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 that
A21: j in dom (Col ((FinS2MX (KL (#) M)),i)) and
A22: j <> i ; :: thesis: (Col ((FinS2MX (KL (#) M)),i)) . j = 0. K
A23: dom (Col ((FinS2MX (KL (#) M)),i)) = Seg (len b2) by A5, A17, A15, FINSEQ_1:def 3;
then A24: [j,i] in [:(Seg (len b2)),(Seg (len b2)):] by A11, A21, ZFMISC_1:87;
A25: Line ((FinS2MX (KL (#) M)),j) = (KL (#) M) . j by A5, A17, A21, A23, MATRIX_0:52
.= (KL . (M /. j)) * (M /. j) by A16, A21, VECTSP_6:def 5 ;
A26: (Col ((FinS2MX (KL (#) M)),i)) . j = (FinS2MX (KL (#) M)) * (j,i) by A16, A21, MATRIX_0:def 8
.= (Line ((FinS2MX (KL (#) M)),j)) . i by A11, A20, MATRIX_0:def 7 ;
A27: (Line ((1. (K,(len b2))),j)) . i = (1. (K,(len b2))) * (j,i) by A11, A13, MATRIX_0:def 7
.= 0. K by A9, A22, A24, MATRIX_1:def 3 ;
M /. j = M . j by A16, A18, A21, PARTFUN1:def 6
.= Line ((1. (K,(len b2))),j) by A1, A21, A23, MATRIX_0:52 ;
hence (Col ((FinS2MX (KL (#) M)),i)) . j = ((KL . (M /. j)) * (Line ((1. (K,(len b2))),j))) . i by A13, A26, A25, MATRIX13:102
.= (KL . (M /. j)) * (0. K) by A11, A13, A27, FVSUM_1:51
.= 0. K ;
:: thesis: verum

end;

then A28: (Col ((FinS2MX (KL (#) M)),i)) . i = Sum (Col ((FinS2MX (KL (#) M)),i)) by A19, MATRIX_3:12
.= v1 . i by A1, A2, A11, A8, MATRIX13:105, MATRIX13:107 ;
A29: Line ((FinS2MX (KL (#) M)),i) = (KL (#) M) . i by A5, A11, A17, MATRIX_0:52
.= (KL . (M /. i)) * (M /. i) by A19, A16, VECTSP_6:def 5 ;
A30: (Col ((FinS2MX (KL (#) M)),i)) . i = (FinS2MX (KL (#) M)) * (i,i) by A19, A16, MATRIX_0:def 8
.= (Line ((FinS2MX (KL (#) M)),i)) . i by A11, A20, MATRIX_0:def 7 ;
M /. i = M . i by A19, A16, A18, PARTFUN1:def 6
.= Line ((1. (K,(len b2))),i) by A1, A11, MATRIX_0:52 ;
then (Col ((FinS2MX (KL (#) M)),i)) . i = ((KL . (M /. i)) * (Line ((1. (K,(len b2))),i))) . i by A30, A13, A29, MATRIX13:102
.= (KL . (M /. i)) * (1_ K) by A11, A13, A14, FVSUM_1:51
.= KL . (M /. i) ;
hence t1 . i = (v1 |-- M) /. i by A3, A4, A6, A5, A10, A28
.= (v1 |-- M) . i by A19, A16, A18, A7, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence v1 |-- M = v1 by A4, A6, A5, FINSEQ_1:14; :: thesis: verum