let F be Field; :: thesis: for V being VectSp of F
for X being Subset of V holds
( X is linearly-independent iff for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 )
let V be VectSp of F; :: thesis: for X being Subset of V holds
( X is linearly-independent iff for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 )
let X be Subset of V; :: thesis: ( X is linearly-independent iff for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 )

A: now :: thesis: ( X is linearly-independent implies for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 )

assume A1: X is linearly-independent ; :: thesis: for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2

now :: thesis: for KL1, KL2 being Linear_Combination of X st Sum KL1 = Sum KL2 holds
KL1 = KL2

let KL1, KL2 be Linear_Combination of X; :: thesis: ( Sum KL1 = Sum KL2 implies KL1 = KL2 )
A2: Carrier KL1 c= X by VECTSP_6:def 4;
Carrier KL2 c= X by VECTSP_6:def 4;
then A3: (Carrier KL1) \/ (Carrier KL2) c= X by A2, XBOOLE_1:8;
assume Sum KL1 = Sum KL2 ; :: thesis: KL1 = KL2
then (Sum KL1) - (Sum KL2) = 0. V by RLVECT_1:5;
then A4: ( KL1 - KL2 is Linear_Combination of Carrier (KL1 - KL2) & Sum (KL1 - KL2) = 0. V ) by VECTSP_6:47, VECTSP_6:def 4;
Carrier (KL1 - KL2) c= (Carrier KL1) \/ (Carrier KL2) by VECTSP_6:41;
then A5: Carrier (KL1 - KL2) is linearly-independent by A1, A3, XBOOLE_1:1, VECTSP_7:1;

now :: thesis: for v being Vector of V holds KL1 . v = KL2 . v

let v be Vector of V; :: thesis: KL1 . v = KL2 . v
not v in Carrier (KL1 - KL2) by VECTSP_7:def 1, A5, A4;
then (KL1 - KL2) . v = 0. F by VECTSP_6:2;
then (KL1 . v) - (KL2 . v) = 0. F by VECTSP_6:40;
hence KL1 . v = KL2 . v by RLVECT_1:21; :: thesis: verum

end;

hence KL1 = KL2 ; :: thesis: verum

end;

hence for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 ; :: thesis: verum

end;

now :: thesis: ( ( for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 ) implies X is linearly-independent )

assume A1: for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 ; :: thesis: X is linearly-independent

now :: thesis: for l being Linear_Combination of X st Sum l = 0. V holds
Carrier l = {}

let l be Linear_Combination of X; :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume A2: Sum l = 0. V ; :: thesis: Carrier l = {}
A3: Sum (ZeroLC V) = 0. V by VECTSP_6:15;
Carrier (ZeroLC V) c= X by VECTSP_6:def 3;
then ZeroLC V is Linear_Combination of X by VECTSP_6:def 4;
hence Carrier l = {} by A1, A2, A3, VECTSP_6:def 3; :: thesis: verum

end;

hence X is linearly-independent by VECTSP_7:def 1; :: thesis: verum

end;

hence ( X is linearly-independent iff for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 ) by A; :: thesis: verum