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 ) and
A2: 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 A3: dom (v |-- b1) = dom b1 by FINSEQ_3:31;
then A4: dom b1 = dom (lmlt (v |-- b1),b1) by Th16;
len (KL (#) b1) = len b1 by VECTSP_6:def 8
.= len (lmlt (v |-- b1),b1) by A4, FINSEQ_3:31 ;
then A5: dom (KL (#) b1) = dom (lmlt (v |-- b1),b1) by FINSEQ_3:31;

A6: now

let t be Nat; :: thesis: ( t in dom (lmlt (v |-- b1),b1) implies (KL (#) b1) . t = (lmlt (v |-- b1),b1) . t )
assume A7: t in dom (lmlt (v |-- b1),b1) ; :: thesis: (KL (#) b1) . t = (lmlt (v |-- b1),b1) . t
then A8: b1 /. t = b1 . t by A4, PARTFUN1:def 8;
t in dom (v |-- b1) by A3, A7, Th16;
then A9: t <= len (v |-- b1) by FINSEQ_3:27;
A10: 1 <= t by A7, FINSEQ_3:27;
then A11: (v |-- b1) /. t = (v |-- b1) . t by A9, FINSEQ_4:24;
t in dom (KL (#) b1) by A5, A7;
hence (KL (#) b1) . t = (KL . (b1 /. t)) * (b1 /. t) by VECTSP_6:def 8
.= ((v |-- b1) /. t) * (b1 /. t) by A2, A10, A9
.= the lmult of V1 . ((v |-- b1) . t),(b1 . t) by A8, A11, VECTSP_1:def 24
.= (lmlt (v |-- b1),b1) . t by A7, 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 A5, A6, FINSEQ_1:17 ;
:: thesis: verum