let K be Field; :: thesis: for V being VectSp of K

for a being Element 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 & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

let V be VectSp of K; :: thesis: for a being Element 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 & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

let a be Element 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 & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * 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 & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

let X be Subset of V; :: thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) implies KL1 = a * KL2 )

assume that

A1: ( X is linearly-independent & Carrier KL1 c= X ) and

A2: ( Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) ) ; :: thesis: KL1 = a * KL2

( Carrier (a * KL2) c= X & Sum KL1 = Sum (a * KL2) ) by A2, VECTSP_6:29, VECTSP_6:45;

hence KL1 = a * KL2 by A1, Th5; :: thesis: verum

for a being Element 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 & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

let V be VectSp of K; :: thesis: for a being Element 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 & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

let a be Element 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 & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * 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 & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

let X be Subset of V; :: thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) implies KL1 = a * KL2 )

assume that

A1: ( X is linearly-independent & Carrier KL1 c= X ) and

A2: ( Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) ) ; :: thesis: KL1 = a * KL2

( Carrier (a * KL2) c= X & Sum KL1 = Sum (a * KL2) ) by A2, VECTSP_6:29, VECTSP_6:45;

hence KL1 = a * KL2 by A1, Th5; :: thesis: verum