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;

hence v = Sum (KL (#) b1) by A1, Th20

.= Sum (lmlt ((v |-- b1),b1)) by A5, A6, FINSEQ_1:13 ;

:: thesis: verum

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

b1 is one-to-one
by Def2;(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;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

hence v = Sum (KL (#) b1) by A1, Th20

.= Sum (lmlt ((v |-- b1),b1)) by A5, A6, FINSEQ_1:13 ;

:: thesis: verum