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 Def7;
len (v |-- b1) = len b1 by Def7;
then A3: dom (v |-- b1) = dom b1 by FINSEQ_3:29;
then A4: dom b1 = dom (lmlt ((v |-- b1),b1)) by Th12;
len (KL (#) b1) = len b1 by VECTSP_6:def 5
.= len (lmlt ((v |-- b1),b1)) by A4, FINSEQ_3:29 ;
then A5: dom (KL (#) b1) = dom (lmlt ((v |-- b1),b1)) by FINSEQ_3:29;

A6: now :: thesis: for t being Nat st t in dom (lmlt ((v |-- b1),b1)) holds
(KL (#) b1) . t = (lmlt ((v |-- b1),b1)) . t

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 6;
t in dom (v |-- b1) by A3, A7, Th12;
then A9: t <= len (v |-- b1) by FINSEQ_3:25;
A10: 1 <= t by A7, FINSEQ_3:25;
then A11: (v |-- b1) /. t = (v |-- b1) . t by A9, FINSEQ_4:15;
t in dom (KL (#) b1) by A5, A7;
hence (KL (#) b1) . t = (KL . (b1 /. t)) * (b1 /. t) by VECTSP_6:def 5
.= ((v |-- b1) /. t) * (b1 /. t) by A2, A10, A9
.= the lmult of V1 . (((v |-- b1) . t),(b1 . t)) by A8, A11, VECTSP_1:def 12
.= (lmlt ((v |-- b1),b1)) . t by A7, FUNCOP_1:22 ;
:: thesis: verum

end;

b1 is one-to-one by Def2;
hence v = Sum (KL (#) b1) by A1, Th20
.= Sum (lmlt ((v |-- b1),b1)) by A5, A6, FINSEQ_1:13 ;
:: thesis: verum