let K be Field; :: thesis:
let V1 be finite-dimensional VectSp of K; :: thesis:
let b1 be OrdBasis of V1; :: thesis:
let d be FinSequence of K; :: thesis:
assume A1: len d = len b1 ; :: thesis:
defpred S₁[ Element of V1, Element of K] means ( ( $1 in rng b1 implies for k being Nat st k in dom b1 & b1 /. k = $1 holds
$2 = d /. k ) & ( not $1 in rng b1 implies $2 = 0. K ) );
A2: for v being Element of V1 ex u being Element of K st S₁[v,u]

proof

let v be Element of V1; :: thesis:

per cases ;

suppose A3: v in rng b1 ; :: thesis:

then consider k being Element of NAT such that
A4: ( k in dom b1 & b1 /. k = v ) by PARTFUN2:4;
take u = d /. k; :: thesis:

now

let i be Nat; :: thesis:
assume A5: ( i in dom b1 & b1 /. i = v ) ; :: thesis:
A6: b1 is one-to-one by Def4;
b1 . i = b1 /. k by A4, A5, PARTFUN1:def 8
.= b1 . k by A4, PARTFUN1:def 8 ;
hence u = d /. i by A4, A5, A6, FUNCT_1:def 8; :: thesis:

end;

hence S₁[v,u] by A3; :: thesis:

end;

suppose A7: not v in rng b1 ; :: thesis:

take 0. K ; :: thesis:
thus S₁[v, 0. K] by A7; :: thesis:

end;

consider KL being Function of V1,K such that
A8: for v being Element of V1 holds S₁[v,KL . v] from FUNCT_2:sch 3(A2);

now

take f = KL; :: thesis:
thus ( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis:

end;

then A9: KL in Funcs the carrier of V1,the carrier of K by FUNCT_2:def 2;
reconsider T = rng b1 as finite Subset of V1 by Def4;

now

take T = T; :: thesis:
let v be Element of V1; :: thesis:
assume not v in T ; :: thesis:
hence KL . v = 0. K by A8; :: thesis:

end;

then reconsider KL1 = KL as Linear_Combination of V1 by A9, VECTSP_6:def 4;

now

take KL1 = KL1; :: thesis:
thus A10: for k being Nat st 1 <= k & k <= len d holds
d /. k = KL1 . (b1 /. k) :: thesis:

proof

let k be Nat; :: thesis:
assume ( 1 <= k & k <= len d ) ; :: thesis:
then A11: k in dom b1 by A1, FINSEQ_3:27;
then b1 . k = b1 /. k by PARTFUN1:def 8;
then b1 /. k in rng b1 by A11, FUNCT_1:def 5;
hence d /. k = KL1 . (b1 /. k) by A8, A11; :: thesis:

end;

for x being set st x in Carrier KL1 holds
x in rng b1

proof

let x be set ; :: thesis:
assume A12: x in Carrier KL1 ; :: thesis:
assume A13: not x in rng b1 ; :: thesis:
consider v being Element of V1 such that
A14: ( x = v & KL1 . v <> 0. K ) by A12, VECTSP_6:19;
thus contradiction by A8, A13, A14; :: thesis:

end;

hence A15: Carrier KL1 c= rng b1 by TARSKI:def 3; :: thesis:
A16: b1 is one-to-one by Def4;
A17: dom d = dom b1 by A1, FINSEQ_3:31;
then A18: dom (lmlt d,b1) = dom b1 by Th16;
then A19: len (lmlt d,b1) = len b1 by FINSEQ_3:31
.= len (KL1 (#) b1) by VECTSP_6:def 8 ;

now

let k be Nat; :: thesis:
assume A20: k in dom (lmlt d,b1) ; :: thesis:
then A21: d /. k = d . k by A17, A18, PARTFUN1:def 8;
A22: b1 /. k = b1 . k by A18, A20, PARTFUN1:def 8;
A23: k in dom (KL1 (#) b1) by A19, A20, FINSEQ_3:31;
A24: ( 1 <= k & k <= len d ) by A1, A18, A20, FINSEQ_3:27;
thus (lmlt d,b1) . k = the lmult of V1 . (d . k),(b1 . k) by A20, FUNCOP_1:28
.= (d /. k) * (b1 /. k) by A21, A22, VECTSP_1:def 24
.= (KL1 . (b1 /. k)) * (b1 /. k) by A10, A24
.= (KL1 (#) b1) . k by A23, VECTSP_6:def 8 ; :: thesis:

end;

hence Sum (lmlt d,b1) = Sum (KL1 (#) b1) by A19, NEWTON:3
.= Sum KL1 by A15, A16, Th24 ;
:: thesis:

end;

hence d = (Sum (lmlt d,b1)) |-- b1 by A1, Def9; :: thesis: