let K be Field; :: thesis: for V being VectSp of K
for KL1, KL2 being Linear_Combination of V
for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds
KL1 = KL2
let V be VectSp of K; :: thesis: for KL1, KL2 being Linear_Combination of V
for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds
KL1 = KL2
let KL1, KL2 be Linear_Combination of V; :: thesis: for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds
KL1 = KL2
let X be Subset of V; :: thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 implies KL1 = KL2 )
assume that
A1: X is linearly-independent and
A2: Carrier KL1 c= X and
A3: Carrier KL2 c= X and
A4: Sum KL1 = Sum KL2 ; :: thesis: KL1 = KL2
A5: (Carrier KL1) \/ (Carrier KL2) c= X by A2, A3, XBOOLE_1:8;
Carrier (KL1 - KL2) c= (Carrier KL1) \/ (Carrier KL2) by VECTSP_6:74;
then A6: Carrier (KL1 - KL2) is linearly-independent by A1, A5, VECTSP_7:2, XBOOLE_1:1;
A7: KL1 - KL2 is Linear_Combination of Carrier (KL1 - KL2) by VECTSP_6:28;
(Sum KL1) - (Sum KL2) = 0. V by A4, VECTSP_1:66;
then A8: Sum (KL1 - KL2) = 0. V by VECTSP_6:80;

now

let v be Vector of V; :: thesis: KL1 . v = KL2 . v
not v in Carrier (KL1 - KL2) by A6, A7, A8, VECTSP_7:def 1;
then (KL1 - KL2) . v = 0. K by VECTSP_6:20;
then (KL1 . v) - (KL2 . v) = 0. K by VECTSP_6:73;
hence KL1 . v = KL2 . v by RLVECT_1:35; :: thesis: verum

end;

hence KL1 = KL2 by VECTSP_6:def 10; :: thesis: verum