let K be Field; :: thesis: for a being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v1 being Element of V1 holds (a * v1) |-- b1 = a * (v1 |-- b1)
let a be Element of K; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v1 being Element of V1 holds (a * v1) |-- b1 = a * (v1 |-- b1)
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for v1 being Element of V1 holds (a * v1) |-- b1 = a * (v1 |-- b1)
let b1 be OrdBasis of V1; :: thesis: for v1 being Element of V1 holds (a * v1) |-- b1 = a * (v1 |-- b1)
let v1 be Element of V1; :: thesis: (a * v1) |-- b1 = a * (v1 |-- b1)
set vb = v1 |-- b1;
set avb = (a * v1) |-- b1;
consider L1 being Linear_Combination of V1 such that
A1: ( v1 = Sum L1 & Carrier L1 c= rng b1 ) and
A2: for k being Nat st 1 <= k & k <= len (v1 |-- b1) holds
(v1 |-- b1) /. k = L1 . (b1 /. k) by MATRLIN:def 9;
consider L2 being Linear_Combination of V1 such that
A3: ( a * v1 = Sum L2 & Carrier L2 c= rng b1 ) and
A4: for k being Nat st 1 <= k & k <= len ((a * v1) |-- b1) holds
((a * v1) |-- b1) /. k = L2 . (b1 /. k) by MATRLIN:def 9;
A5: ( len (v1 |-- b1) = len b1 & len ((a * v1) |-- b1) = len b1 & len (a * (v1 |-- b1)) = len (v1 |-- b1) ) by MATRIXR1:16, MATRLIN:def 9;
then reconsider vb' = v1 |-- b1, avb = (a * v1) |-- b1, Avb = a * (v1 |-- b1) as Element of (len b1) -tuples_on the carrier of K by FINSEQ_2:110;
reconsider rb1 = rng b1 as Basis of V1 by MATRLIN:def 4;
A6: rb1 is linearly-independent by VECTSP_7:def 3;

now

let i be Nat; :: thesis: ( i in Seg (len b1) implies avb . i = Avb . i )
assume A7: i in Seg (len b1) ; :: thesis: avb . i = Avb . i
A8: ( 1 <= i & i <= len b1 ) by A7, FINSEQ_1:3;
( dom (v1 |-- b1) = dom b1 & dom avb = dom b1 & dom b1 = Seg (len b1) ) by A5, FINSEQ_1:def 3, FINSEQ_3:31;
then A9: ( (v1 |-- b1) . i = (v1 |-- b1) /. i & avb . i = avb /. i ) by A7, PARTFUN1:def 8;

A10: now

per cases ( a <> 0. K or a = 0. K ) ;

suppose a <> 0. K ; :: thesis: L2 . (b1 /. i) = a * (vb' /. i)

then a * L1 = L2 by A1, A3, A6, MATRLIN:11;
hence L2 . (b1 /. i) = a * (L1 . (b1 /. i)) by VECTSP_6:def 12
.= a * (vb' /. i) by A5, A8, A2 ;
:: thesis: verum

end;

suppose A11: a = 0. K ; :: thesis: L2 . (b1 /. i) = a * (vb' /. i)

then A12: a * v1 = 0. V1 by VECTSP_1:59;
A13: L2 is Linear_Combination of Carrier L2 by VECTSP_6:28;
Carrier L2 is linearly-independent by A3, A6, VECTSP_7:2;
then not b1 /. i in Carrier L2 by A3, A12, A13, VECTSP_7:def 1;
hence L2 . (b1 /. i) = 0. K
.= a * (vb' /. i) by A11, VECTSP_1:39 ;
:: thesis: verum

end;

end;

end;

thus avb . i = L2 . (b1 /. i) by A9, A5, A4, A8
.= Avb . i by A10, A7, A9, FVSUM_1:63 ; :: thesis: verum

end;

hence (a * v1) |-- b1 = a * (v1 |-- b1) by FINSEQ_2:139; :: thesis: verum