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 7;
consider L3 being Linear_Combination of V1 such that
A3: ( v1 + w1 = Sum L3 & Carrier L3 c= rng b1 ) and
A4: for k being Nat st 1 <= k & k <= len ((v1 + w1) |-- b1) holds
((v1 + w1) |-- b1) /. k = L3 . (b1 /. k) by MATRLIN:def 7;
A5: len (w1 |-- b1) = len b1 by MATRLIN:def 7;
reconsider rb1 = rng b1 as Basis of V1 by MATRLIN:def 2;
consider L2 being Linear_Combination of V1 such that
A6: ( w1 = Sum L2 & Carrier L2 c= rng b1 ) and
A7: for k being Nat st 1 <= k & k <= len (w1 |-- b1) holds
(w1 |-- b1) /. k = L2 . (b1 /. k) by MATRLIN:def 7;
A8: len (v1 |-- b1) = len b1 by MATRLIN:def 7;
A9: len ((v1 + w1) |-- b1) = len b1 by MATRLIN:def 7;
then reconsider vb = v1 |-- b1, wb = w1 |-- b1, vwb = (v1 + w1) |-- b1 as Element of (len b1) -tuples_on the carrier of K by A8, A5, FINSEQ_2:92;
rb1 is linearly-independent by VECTSP_7:def 3;
then A10: L3 = L1 + L2 by A1, A6, A3, MATRLIN:6;

now :: thesis: for i being Nat st i in Seg (len b1) holds
vwb . i = (vb + wb) . i

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

end;

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