let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v1, w1 being Element of V1 holds (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for v1, w1 being Element of V1 holds (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
let b1 be OrdBasis of V1; :: thesis: for v1, w1 being Element of V1 holds (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
let v1, w1 be Element of V1; :: thesis: (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
set vb = v1 |-- b1;
set wb = w1 |-- b1;
set vwb = (v1 + w1) |-- 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: ( w1 = Sum L2 & Carrier L2 c= rng b1 ) and
A4: for k being Nat st 1 <= k & k <= len (w1 |-- b1) holds
(w1 |-- b1) /. k = L2 . (b1 /. k) by MATRLIN:def 9;
consider L3 being Linear_Combination of V1 such that
A5: ( v1 + w1 = Sum L3 & Carrier L3 c= rng b1 ) and
A6: for k being Nat st 1 <= k & k <= len ((v1 + w1) |-- b1) holds
((v1 + w1) |-- b1) /. k = L3 . (b1 /. k) by MATRLIN:def 9;
A7: ( len (v1 |-- b1) = len b1 & len (w1 |-- b1) = len b1 & len ((v1 + w1) |-- b1) = len b1 ) by MATRLIN:def 9;
then reconsider vb = v1 |-- b1, wb = w1 |-- b1, vwb = (v1 + w1) |-- 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;
rb1 is linearly-independent by VECTSP_7:def 3;
then A8: L3 = L1 + L2 by A1, A3, A5, MATRLIN:10;

now

let i be Nat; :: thesis: ( i in Seg (len b1) implies vwb . i = (vb + wb) . i )
assume A9: i in Seg (len b1) ; :: thesis: vwb . i = (vb + wb) . i
A10: ( 1 <= i & i <= len b1 ) by A9, FINSEQ_1:3;
( dom vb = dom b1 & dom wb = dom b1 & dom vwb = dom b1 & dom b1 = Seg (len b1) ) by A7, FINSEQ_1:def 3, FINSEQ_3:31;
then A11: ( vb . i = vb /. i & wb . i = wb /. i & vwb . i = vwb /. i ) by A9, PARTFUN1:def 8;
hence vwb . i = (L1 + L2) . (b1 /. i) by A7, A10, A6, A8
.= (L1 . (b1 /. i)) + (L2 . (b1 /. i)) by VECTSP_6:def 11
.= (vb /. i) + (L2 . (b1 /. i)) by A7, A10, A2
.= (vb /. i) + (wb /. i) by A7, A10, A4
.= (vb + wb) . i by A9, A11, FVSUM_1:22 ;
:: thesis: verum

end;

hence (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1) by FINSEQ_2:139; :: thesis: verum