let K be Field; :: thesis: for V being VectSp of K
for A being linearly-independent Subset of V
for L1, L2 being Linear_Combination of V st Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 holds
L1 = L2
let V be VectSp of K; :: thesis: for A being linearly-independent Subset of V
for L1, L2 being Linear_Combination of V st Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 holds
L1 = L2
let A be linearly-independent Subset of V; :: thesis: for L1, L2 being Linear_Combination of V st Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 holds
L1 = L2
let L1, L2 be Linear_Combination of V; :: thesis: ( Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 implies L1 = L2 )
assume that
A1: ( Carrier L1 c= A & Carrier L2 c= A ) and
A2: Sum L1 = Sum L2 ; :: thesis: L1 = L2
( L1 is Linear_Combination of A & L2 is Linear_Combination of A ) by A1, VECTSP_6:def 4;
then A3: L1 - L2 is Linear_Combination of A by VECTSP_6:42;
Sum (L1 - L2) = (Sum L1) - (Sum L2) by VECTSP_6:47
.= 0. V by A2, RLVECT_1:15 ;
then Carrier (L1 - L2) = {} by A3, VECTSP_7:def 1;
then ZeroLC V = L1 - L2 by VECTSP_6:def 3
.= L1 + (- L2) by VECTSP_6:def 11
.= (- L2) + L1 by VECTSP_6:25 ;
then L1 = - (- L2) by VECTSP_6:37;
hence L1 = L2 ; :: thesis: verum