let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v being Element of V1 holds v = Sum (lmlt (v |-- b1),b1)
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for v being Element of V1 holds v = Sum (lmlt (v |-- b1),b1)
let b1 be OrdBasis of V1; :: thesis: for v being Element of V1 holds v = Sum (lmlt (v |-- b1),b1)
let v be Element of V1; :: thesis: v = Sum (lmlt (v |-- b1),b1)
consider KL being Linear_Combination of V1 such that
A1: ( v = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len (v |-- b1) holds
(v |-- b1) /. k = KL . (b1 /. k) ) ) by Def9;
len (v |-- b1) = len b1 by Def9;
then A2: dom (v |-- b1) = dom b1 by FINSEQ_3:31;
then A3: dom b1 = dom (lmlt (v |-- b1),b1) by Th16;
A4: len (KL (#) b1) = len b1 by VECTSP_6:def 8
.= len (lmlt (v |-- b1),b1) by A3, FINSEQ_3:31 ;

A5: now

let t be Nat; :: thesis: ( t in dom (lmlt (v |-- b1),b1) implies (KL (#) b1) . t = (lmlt (v |-- b1),b1) . t )
assume A6: t in dom (lmlt (v |-- b1),b1) ; :: thesis: (KL (#) b1) . t = (lmlt (v |-- b1),b1) . t
then A7: t in dom (KL (#) b1) by A4, FINSEQ_3:31;
t in dom (v |-- b1) by A2, A6, Th16;
then A8: ( 1 <= t & t <= len (v |-- b1) ) by FINSEQ_3:27;
A9: b1 /. t = b1 . t by A3, A6, PARTFUN1:def 8;
A10: (v |-- b1) /. t = (v |-- b1) . t by A8, FINSEQ_4:24;
thus (KL (#) b1) . t = (KL . (b1 /. t)) * (b1 /. t) by A7, VECTSP_6:def 8
.= ((v |-- b1) /. t) * (b1 /. t) by A1, A8
.= the lmult of V1 . ((v |-- b1) . t),(b1 . t) by A9, A10, VECTSP_1:def 24
.= (lmlt (v |-- b1),b1) . t by A6, FUNCOP_1:28 ; :: thesis: verum

end;

b1 is one-to-one by Def4;
hence v = Sum (KL (#) b1) by A1, Th24
.= Sum (lmlt (v |-- b1),b1) by A4, A5, NEWTON:3 ;
:: thesis: verum