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 and
A2: Carrier KL1 c= X and
A3: Carrier KL2 c= X and
A4: Carrier KL3 c= X and
A5: Sum KL1 = (Sum KL2) + (Sum KL3) ; :: thesis: KL1 = KL2 + KL3
A6: Carrier (KL2 + KL3) c= (Carrier KL2) \/ (Carrier KL3) by VECTSP_6:51;
(Carrier KL2) \/ (Carrier KL3) c= X by A3, A4, XBOOLE_1:8;
then A7: Carrier (KL2 + KL3) c= X by A6, XBOOLE_1:1;
Sum KL1 = Sum (KL2 + KL3) by A5, VECTSP_6:77;
hence KL1 = KL2 + KL3 by A1, A2, A7, Th9; :: thesis: verum