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 and
A2: Carrier KL1 c= X and
A3: Carrier KL2 c= X and
A4: a <> 0. K and
A5: Sum KL1 = a * (Sum KL2) ; :: thesis: KL1 = a * KL2
A6: Carrier (a * KL2) c= X by A3, A4, VECTSP_6:59;
Sum KL1 = Sum (a * KL2) by A5, VECTSP_6:78;
hence KL1 = a * KL2 by A1, A2, A6, Th9; :: thesis: verum