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

for KL1, KL2, KL3 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

let V be VectSp of K; :: thesis: for KL1, KL2, KL3 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

let KL1, KL2, KL3 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 & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

let X be Subset of V; :: thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) implies KL1 = KL2 + KL3 )

assume that

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

A2: ( Carrier KL2 c= X & Carrier KL3 c= X ) and

A3: Sum KL1 = (Sum KL2) + (Sum KL3) ; :: thesis: KL1 = KL2 + KL3

( Carrier (KL2 + KL3) c= (Carrier KL2) \/ (Carrier KL3) & (Carrier KL2) \/ (Carrier KL3) c= X ) by A2, VECTSP_6:23, XBOOLE_1:8;

then A4: Carrier (KL2 + KL3) c= X ;

Sum KL1 = Sum (KL2 + KL3) by A3, VECTSP_6:44;

hence KL1 = KL2 + KL3 by A1, A4, Th5; :: thesis: verum

for KL1, KL2, KL3 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

let V be VectSp of K; :: thesis: for KL1, KL2, KL3 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

let KL1, KL2, KL3 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 & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

let X be Subset of V; :: thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) implies KL1 = KL2 + KL3 )

assume that

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

A2: ( Carrier KL2 c= X & Carrier KL3 c= X ) and

A3: Sum KL1 = (Sum KL2) + (Sum KL3) ; :: thesis: KL1 = KL2 + KL3

( Carrier (KL2 + KL3) c= (Carrier KL2) \/ (Carrier KL3) & (Carrier KL2) \/ (Carrier KL3) c= X ) by A2, VECTSP_6:23, XBOOLE_1:8;

then A4: Carrier (KL2 + KL3) c= X ;

Sum KL1 = Sum (KL2 + KL3) by A3, VECTSP_6:44;

hence KL1 = KL2 + KL3 by A1, A4, Th5; :: thesis: verum