let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for d being FinSequence of K st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for d being FinSequence of K st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1
let b1 be OrdBasis of V1; :: thesis: for d being FinSequence of K st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1
let d be FinSequence of K; :: thesis: ( len d = len b1 implies d = (Sum (lmlt (d,b1))) |-- b1 )
reconsider T = rng b1 as finite Subset of V1 by Def2;
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 ) );
A1: for v being Element of V1 ex u being Element of K st S₁[v,u]

proof

let v be Element of V1; :: thesis: ex u being Element of K st S₁[v,u]

per cases ( v in rng b1 or not v in rng b1 ) ;

suppose A2: v in rng b1 ; :: thesis: ex u being Element of K st S₁[v,u]

then consider k being Element of NAT such that
A3: k in dom b1 and
A4: b1 /. k = v by PARTFUN2:2;
take u = d /. k; :: thesis: S₁[v,u]

now :: thesis: for i being Nat st i in dom b1 & b1 /. i = v holds
u = d /. i

A5: b1 is one-to-one by Def2;
let i be Nat; :: thesis: ( i in dom b1 & b1 /. i = v implies u = d /. i )
assume that
A6: i in dom b1 and
A7: b1 /. i = v ; :: thesis: u = d /. i
b1 . i = b1 /. k by A4, A6, A7, PARTFUN1:def 6
.= b1 . k by A3, PARTFUN1:def 6 ;
hence u = d /. i by A3, A6, A5, FUNCT_1:def 4; :: thesis: verum

end;

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

end;

suppose A8: not v in rng b1 ; :: thesis: ex u being Element of K st S₁[v,u]

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

end;

end;

end;

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

A10: now :: thesis: ex T being finite Subset of V1 st
for v being Element of V1 st not v in T holds
KL . v = 0. K

take T = T; :: thesis: for v being Element of V1 st not v in T holds
KL . v = 0. K
let v be Element of V1; :: thesis: ( not v in T implies KL . v = 0. K )
assume not v in T ; :: thesis: KL . v = 0. K
hence KL . v = 0. K by A9; :: thesis: verum

end;

now :: thesis: ex f being Function of V1,K st
( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K )

take f = KL; :: thesis: ( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K )
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: verum

end;

then KL in Funcs ( the carrier of V1, the carrier of K) by FUNCT_2:def 2;
then reconsider KL1 = KL as Linear_Combination of V1 by A10, VECTSP_6:def 1;
assume A11: len d = len b1 ; :: thesis: d = (Sum (lmlt (d,b1))) |-- b1

now :: thesis: ex KL1 being Linear_Combination of V1 st
( ( for k being Nat st 1 <= k & k <= len d holds
d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

take KL1 = KL1; :: thesis: ( ( for k being Nat st 1 <= k & k <= len d holds
d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )
A12: b1 is one-to-one by Def2;
thus A13: for k being Nat st 1 <= k & k <= len d holds
d /. k = KL1 . (b1 /. k) :: thesis: ( Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len d implies d /. k = KL1 . (b1 /. k) )
assume ( 1 <= k & k <= len d ) ; :: thesis: d /. k = KL1 . (b1 /. k)
then A14: k in dom b1 by A11, FINSEQ_3:25;
then b1 . k = b1 /. k by PARTFUN1:def 6;
then b1 /. k in rng b1 by A14, FUNCT_1:def 3;
hence d /. k = KL1 . (b1 /. k) by A9, A14; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in Carrier KL1 implies x in rng b1 )
assume x in Carrier KL1 ; :: thesis: x in rng b1
then A15: ex v being Element of V1 st
( x = v & KL1 . v <> 0. K ) by VECTSP_6:1;
assume not x in rng b1 ; :: thesis: contradiction
hence contradiction by A9, A15; :: thesis: verum

end;

hence A16: Carrier KL1 c= rng b1 ; :: thesis: Sum (lmlt (d,b1)) = Sum KL1
A17: dom d = dom b1 by A11, FINSEQ_3:29;
then A18: dom (lmlt (d,b1)) = dom b1 by Th12;
then A19: len (lmlt (d,b1)) = len b1 by FINSEQ_3:29
.= len (KL1 (#) b1) by VECTSP_6:def 5 ;

now :: thesis: for k being Nat st k in dom (lmlt (d,b1)) holds
(lmlt (d,b1)) . k = (KL1 (#) b1) . k

let k be Nat; :: thesis: ( k in dom (lmlt (d,b1)) implies (lmlt (d,b1)) . k = (KL1 (#) b1) . k )
assume A20: k in dom (lmlt (d,b1)) ; :: thesis: (lmlt (d,b1)) . k = (KL1 (#) b1) . k
then A21: k in dom (KL1 (#) b1) by A19, FINSEQ_3:29;
A22: ( 1 <= k & k <= len d ) by A11, A18, A20, FINSEQ_3:25;
A23: ( d /. k = d . k & b1 /. k = b1 . k ) by A17, A18, A20, PARTFUN1:def 6;
thus (lmlt (d,b1)) . k = the lmult of V1 . ((d . k),(b1 . k)) by A20, FUNCOP_1:22
.= (d /. k) * (b1 /. k) by A23, VECTSP_1:def 12
.= (KL1 . (b1 /. k)) * (b1 /. k) by A13, A22
.= (KL1 (#) b1) . k by A21, VECTSP_6:def 5 ; :: thesis: verum

end;

hence Sum (lmlt (d,b1)) = Sum (KL1 (#) b1) by A19, FINSEQ_2:9
.= Sum KL1 by A16, A12, Th20 ;
:: thesis: verum

end;

hence d = (Sum (lmlt (d,b1))) |-- b1 by A11, Def7; :: thesis: verum